io7m | single-page | multi-page | Montarre User Manual 1.0.0-SNAPSHOT
6.5. com.io7m.montarre.shell
Previous
Front Matter
Up
Front Matter
Next

# 7. Package Format 1.0 Specification

- 7.1. Overview
- 7.2. Regular Expressions
- 7.3. Dotted Strings
- 7.4. Language
- 7.5. TranslatedText
- 7.6. Hash
  - 7.6.1. Overview
  - 7.6.2. Algorithm
  - 7.6.3. Value
- 7.7. Architecture Name
- 7.8. Operating System Name
- 7.9. Platform
- 7.10. Package
- 7.11. Metadata
  - 7.11.1. Overview
  - 7.11.2. ApplicationKind
  - 7.11.3. Categories
  - 7.11.4. Copying
    - 7.11.4.1. Overview
    - 7.11.4.2. License
    - 7.11.4.3. Copyright
  - 7.11.5. Description
  - 7.11.6. Flatpak
    - 7.11.6.1. Overview
    - 7.11.6.2. Runtimes
    - 7.11.6.3. Permissions
  - 7.11.7. JavaInfo
    - 7.11.7.1. Overview
    - 7.11.7.2. Required JDK Version
    - 7.11.7.3. Main Module
    - 7.11.7.4. JDK Runtime Image Type
    - 7.11.7.5. Native Access
    - 7.11.7.6. Extra Options
  - 7.11.8. Links
    - 7.11.8.1. Overview
    - 7.11.8.2. Roles
  - 7.11.9. LongDescription
    - 7.11.9.1. Overview
    - 7.11.9.2. Paragraph
    - 7.11.9.3. Feature
  - 7.11.10. Names
    - 7.11.10.1. Overview
    - 7.11.10.2. Package Name
    - 7.11.10.3. Human Name
    - 7.11.10.4. Short Name
  - 7.11.11. Vendor
    - 7.11.11.1. Overview
    - 7.11.11.2. Name
    - 7.11.11.3. ID
  - 7.11.12. Version
    - 7.11.12.1. Overview
    - 7.11.12.2. Number
    - 7.11.12.3. Date
- 7.12. Manifest
  - 7.12.1. Overview
  - 7.12.2. FileName
  - 7.12.3. Size
  - 7.12.4. Modules
  - 7.12.5. PlatformModules
  - 7.12.6. Resources
- 7.13. Serialization
  - 7.13.1. Overview
  - 7.13.2. Entomos
  - 7.13.3. XML
  - 7.13.4. XML Schema
- 7.14. Model Sources

## 7.1. Overview

1
This section specifies the format of version 1.0 montarre packages.
2
This specification is divided into an abstract model and a separate serialization. The purpose of the model is to describe the semantics of montarre packages; the actual meaning of the data within, and to describe properties and invariants that must be true for all valid montarre packages. The serialization section describes the on-disk formats used for distribution.
3
The formal specification described here is written in the Gallina specification language of the Rocq theorem prover. The language is a total, pure-functional, dependently-typed language allowing for describing systems in rigorous detail including machine-checked proofs of various chosen properties.
4
The full sources of the entire specification are published at the end of this section.

## 7.2. Regular Expressions

1
The specification makes use of regular expressions to specify the required formats of some string types. The regular expression language used should be assumed to be the Java regular expression language.
2
The specification itself axiomatizes regular expressions using the following definitions:

### 7.2.3. RegularExpressionT

    (** The opaque, abstract type of regular expressions. *)
    Parameter RegularExpressionT : string -> Set.

### 7.2.4. regex

    (** For the sake of specification simplicity, we assume that all
        strings are valid regular expressions. *)
    Parameter regex : forall (s : string), RegularExpressionT s.

### 7.2.5. matches

    (** A proposition that states that a given regular expression
        matches a given string. *)
    Parameter matches : forall (s : string) {e : string},
      RegularExpressionT e -> Prop.

### 7.2.6. matchesDecidable

    (** Whether a string matches a regular expression is decidable. *)
    Parameter matchesDecidable : forall
      (s : string)
      {e : string}
      (r : RegularExpressionT e),
        {matches s r}+{~matches s r}.

## 7.3. Dotted Strings

1
A Lanark dotted string is a string conforming to the regular expression given in the Lanark specification.

### 7.3.2. Dotted String

    Definition lanarkDottedString :=
      forall (s : string),
        matches s (regex "([a-z][a-z0-9_-]{0,63})(\.[a-z][a-z0-9_-]{0,62}){0,15}").

## 7.4. Language

1
A language value is an IETF BCP 47 language tag identifying a language.

### 7.4.2. Language

    Definition LanguageT :=
      string.

3
Example language values include: "en", "yi-Hebr", "gsw-u-sd-chzh".

## 7.5. TranslatedText

1
A translated text value is a record consisting of a piece of text in a specified language, along with a map consisting of translations of that text indexed by language.

### 7.5.2. Translated Text

    Inductive TranslatedTextT := TranslatedText {
      language     : LanguageT;
      text         : string;
      translations : LanguageMaps.t string
    }.

## 7.6. Hash

## 7.6.1. Overview

1
A hash is a record consisting of an algorithm and a value.

### 7.6.1.2. Hash

    Inductive HashT := Hash {
      hashAlgorithm : HashAlgorithmT;
      hashValue     : HashValueT
    }.

## 7.6.2. Algorithm

1
A hash algorithm specifies the name of a cryptographic hash algorithm. The names must be taken from the Java message digest algorithm name specification.

### 7.6.2.2. Algorithm

    Definition HashAlgorithmT :=
      string.

## 7.6.3. Value

1
A hash value is an ASCII, lowercase, hexadecimal text serialization of the binary output of a hash algorithm.

### 7.6.3.2. Value

    Inductive HashValueT :=
      HashValue : forall (s : string),
        matches s (regex "[a-f0-9]{2,256}")
          -> HashValueT.

## 7.7. Architecture Name

1
An architecture name is a unique name for a particular hardware architecture. It represents an attempt to provide a consistent naming convention for hardware types[3].
2
An architecture name is a string conforming to the regular expression [a-z][a-z0-9_-]{0,32}.

### 7.7.3. Architecture Name

    Inductive ArchitectureNameT :=
      ArchitectureName : forall (s : string),
        matches s (regex "[a-z][a-z0-9_-]{0,32}")
          -> ArchitectureNameT.

4
This specification recognizes the following architecture names:

### 7.7.5. Architecture Names

Name | Description
--- | ---
aarch_64 | 64-bit ARM
arm_32 | 32-bit ARM
loongarch_64 | 64-bit LoongArch
mips_32 | 32-bit MIPS
mips_64 | 64-bit MIPS
mipsle_32 | 32-bit little-endian MIPS
mipsle_64 | 64-bit little-endian MIPS
ppc_32 | 32-bit PowerPC
ppc_64 | 64-bit PowerPC
ppcle_32 | 32-bit little-endian PowerPC
ppcle_64 | 64-bit little-endian PowerPC
riscv_32 | 32-bit RISC-V
riscv_64 | 64-bit RISC-V
s390_64 | 64-bit IBM z/Architecture
sparc_32 | 32-bit SPARC
sparc_64 | 64-bit SPARC
x86_32 | 32-bit x86
x86_64 | 64-bit x86

6
The special name unknown is assigned to unrecognized hardware architectures. The unknown name is not permitted to appear in package declarations.

## 7.8. Operating System Name

1
An operating system name is a unique name for a particular operating system. It represents an attempt to provide a consistent naming convention for operating systems.
2
An operating system name is a string conforming to the regular expression [a-z][a-z0-9_-]{0,32}.

### 7.8.3. Operating System Name

    Inductive OperatingSystemNameT :=
      OperatingSystemName : forall (s : string),
        matches s (regex "[a-z][a-z0-9_-]{0,32}")
          -> OperatingSystemNameT.

4
This specification recognizes the following operating system names:

### 7.8.5. Architecture Names

Name | Description
--- | ---
aix | IBM AIX
freebsd | FreeBSD
hpux | HP-UX
linux | Linux
netbsd | NetBSD
openbsd | OpenBSD
os400 | IBM i
osx | MacOS
solaris | Oracle Solaris
windows | Microsoft Windows

6
The special name unknown is assigned to unrecognized operating systems. The unknown name is not permitted to appear in package declarations.

## 7.9. Platform

1
A platform is a record consisting of an architecture name and operating system name.

### 7.9.2. Platform

    Inductive PlatformT := Platform {
      platformArch : ArchitectureNameT;
      platformOS   : OperatingSystemNameT
    }.

## 7.10. Package

1
A montarre package contains a single package declaration which specifies metadata and a manifest.

## 7.11. Metadata

## 7.11.1. Overview

1
The metadata for the package is a record describing the package itself. It provides important information pertaining to the identity of the package, information pertaining to the runtime environment required to run the package, and information used to produce listings in packaging environments such as Flatpak.

### 7.11.1.2. Metadata

    Inductive MetadataT := Metadata {
      metaApplicationKind  : ApplicationKindT;
      metaCategories       : list CategoryT;
      metaCopying          : CopyingT;
      metaDescription      : DescriptionT;
      metaFlatpak          : FlatpakT;
      metaJavaInfo         : JavaInfoT;
      metaLinks            : list LinkT;
      metaLongDescriptions : LanguageMaps.t LongDescriptionT;
      metaNames            : NamesT;
      metaVendor           : VendorT;
      metaVersion          : VersionT
    }.

## 7.11.2. ApplicationKind

1
The application kind of a package is one of the following values:

### 7.11.2.2. ApplicationKind

Value | Description
--- | ---
CONSOLE | The application is a text-only console application.
GRAPHICAL | The application is a graphical application.

### 7.11.2.3. Application Kind

    Inductive ApplicationKindT :=
      | CONSOLE
      | GRAPHICAL
      .

## 7.11.3. Categories

1
A category is a string conforming to the regular expression [A-Z][A-Za-z0-9_-]{0,128}. A package has zero or more categories.

### 7.11.3.2. Category

    Inductive CategoryT :=
      Category : forall (s : string),
        matches s (regex "[A-Z][A-Za-z0-9_-]{0,128}")
          -> CategoryT.

3
Categories should be taken from the Freedesktop.org category registry.
4
Example category values include: "Building", "Development".

## 7.11.4. Copying

## 7.11.4.1. Overview

1
The copying information for a package is a record consisting of a license and a copyright.

### 7.11.4.1.2. Copying

    Inductive CopyingT := Copying {
      license   : LicenseT;
      copyright : CopyrightT
    }.

## 7.11.4.2. License

1
A license is an SPDX license identifier denoting the license of the package.

### 7.11.4.2.2. License

    Definition LicenseT :=
      string.

3
Example license values include: "ISC", "Apache-2.0", "BSD-3-Clause", "GPL-3.0-or-later".

## 7.11.4.3. Copyright

1
A copyright is a simple copyright string that indicates the current holder of the copyright on the package.

### 7.11.4.3.2. Copyright

    Definition CopyrightT :=
      string.

3
An example copyright value is: "Copyright © 2024 Mark Raynsford <code@io7m.com> https://www.io7m.com".

## 7.11.5. Description

1
A description is a short translated text that provides a summary of the package.

### 7.11.5.2. Description

    Definition DescriptionT :=
      TranslatedTextT.

## 7.11.6. Flatpak

## 7.11.6.1. Overview

1
The Flatpak information for a package provides extra metadata used to produce Flatpaks.

### 7.11.6.1.2. Flatpak

    Inductive FlatpakT := Flatpak {
      flatpakPermissions : list FlatpakPermissionT;
      flatpakRuntimes    : list FlatpakRuntimeT
    }.

## 7.11.6.2. Runtimes

1
A Flatpak runtime consists of a name, a version, and a role.

### 7.11.6.2.2. Flatpak Runtime

    Inductive FlatpakRuntimeT := FlatpakRuntime {
      flatpakRuntimeName    : string;
      flatpakRuntimeVersion : string;
      flatpakRuntimeRole    : FlatpakRuntimeRoleT
    }.

3
Roles may be one of the following values:

### 7.11.6.2.4. Flatpak Roles

Value | Description
--- | ---
SDK | A runtime for building applications.
PLATFORM | A runtime for running applications.

### 7.11.6.2.5. Flatpak Runtime Role

    Inductive FlatpakRuntimeRoleT :=
      | SDK
      | PLATFORM
      .

## 7.11.6.3. Permissions

1
A Flatpak permission denotes that the named permission will be granted to the application when it runs as a Flatpak.

### 7.11.6.3.2. Flatpak Permission

    Definition FlatpakPermissionT :=
      string.

3
Example permission values include: "--share=net", "--socket=x11".

## 7.11.7. JavaInfo

## 7.11.7.1. Overview

1
The java info information for a package is a record consisting of metadata describing the application's required JDK version, main module, JDK runtime image type, and any native access and extra options.

### 7.11.7.1.2. Java Info

    Inductive JavaInfoT := JavaInfo {
      requiredJDKVersion : nat;
      mainModule         : string;
      extraOptions       : list string;
      enableNativeAccess : list string;
      imageType          : JavaImageT
    }.

## 7.11.7.2. Required JDK Version

1
The required JDK version specifies the lower bound of the major version of the Java runtime required to use this package.

## 7.11.7.3. Main Module

1
The main module specifies the fully-qualified name of the application's main class.
2
An example main module value is: "com.io7m.montarre.cmdline/com.io7m.montarre.cmdline.MMain".

## 7.11.7.4. JDK Runtime Image Type

1
The JDK runtime image type specifies the type of runtime image the application needs in order to run.

### 7.11.7.4.2. JavaImageT

    Inductive JavaImageT :=
        JDK
      | JRE.

3
A value of JDK indicates the application requires the full set of jdk.* modules to be present.
4
A value of JRE indicates the application can work without the jdk.* modules.

## 7.11.7.5. Native Access

1
The enableNativeAccess list specifies a list of modules that are permitted to use the Java FFI.

## 7.11.7.6. Extra Options

1
The extraOptions list specifies a list of extra options that will be passed to the Java runtime on application startup.

## 7.11.8. Links

## 7.11.8.1. Overview

1
A link is a target reference to an external website or entity, along with a role describing the relationship between that entity and the package.
2
The target of a link must be a valid RFC 3986 URI.

### 7.11.8.1.3. Link

    Inductive LinkT := Link {
      linkRole   : LinkRoleT;
      linkTarget : string
    }.

## 7.11.8.2. Roles

1
A role is one of the following values:

### 7.11.8.2.2. Role Values

Value | Description
--- | ---
ISSUES | A link to an issue tracker.
HOME_PAGE | A link to a home page.
DONATION | A link to a donation page.
CONTACT | A link to a contact page.
FAQ | A link to an FAQ page.
TRANSLATE | A link to a translation page.
CONTRIBUTE | A link to a contribution page.
SCM | A link to an SCM repository.

### 7.11.8.2.3. Link Role

    Inductive LinkRoleT :=
      | ISSUES
      | HOME_PAGE
      | DONATION
      | CONTACT
      | FAQ
      | TRANSLATE
      | CONTRIBUTE
      | SCM
      .

## 7.11.9. LongDescription

## 7.11.9.1. Overview

1
The long description information for a package is a set of paragraphs and features. A long description has an associated language and there may be at most one long description per language in a given package.

### 7.11.9.1.2. Long Description

    Inductive LongDescriptionT := LongDescription {
      descriptionLanguage : LanguageT;
      descriptions        : list ParagraphT;
      features            : list FeatureT
    }.

## 7.11.9.2. Paragraph

1
A paragraph is a humanly readable description of some aspect of the package for marketing purposes.

### 7.11.9.2.2. Paragraph

    Definition ParagraphT :=
      string.

## 7.11.9.3. Feature

1
A feature is a humanly readable description of one of the features provided by the package for marketing purposes.

### 7.11.9.3.2. Feature

    Definition FeatureT :=
      string.

## 7.11.10. Names

## 7.11.10.1. Overview

1
The names information for a package is a record consisting of a set of different types of names for the package.

### 7.11.10.1.2. Names

    Inductive NamesT := Names {
      namePackage : PackageNameT;
      nameShort   : ShortNameT;
      nameHuman   : HumanNameT
    }.

## 7.11.10.2. Package Name

1
The package name is a unique identifier for the package, specified as a dotted string.

### 7.11.10.2.2. Package Name

    Definition PackageNameT :=
      lanarkDottedString.

3
Example package name values include: "com.io7m.montarre", "com.io7m.lanark".

## 7.11.10.3. Human Name

1
The human name is a friendly, human-readable name for the package.

### 7.11.10.3.2. Human Name

    Definition HumanNameT :=
      string.

3
An example human name value is "Montarre".

## 7.11.10.4. Short Name

1
The short name is a name conforming to the regular expression [a-z][a-z0-9_-]{0,128} [2].

### 7.11.10.4.2. Short Name

    Inductive ShortNameT :=
      ShortName : forall (s : string),
        matches s (regex "[a-z][a-z0-9_-]{0,128}")
          -> ShortNameT.

3
An example short name value is "montarre".

## 7.11.11. Vendor

## 7.11.11.1. Overview

1
The vendor information for a package is a record consisting of a vendor name and a unique vendor ID.

### 7.11.11.1.2. Vendor

    Inductive VendorT := Vendor {
      vendorId   : VendorIDT;
      vendorName : VendorNameT
    }.

## 7.11.11.2. Name

1
The vendor name is the humanly-readable name of the vendor of the package, conforming to the regular expression [a-zA-Z][A-Za-z0-9_-]{0,128} [1].

### 7.11.11.2.2. Vendor Name

    Inductive VendorNameT :=
      VendorName : forall (s : string),
        matches s (regex "[a-zA-Z][A-Za-z0-9_-]{0,128}")
          -> VendorNameT.

## 7.11.11.3. ID

1
The vendor ID is a unique identifier for the vendor of the package, specified as a dotted string.

### 7.11.11.3.2. Vendor ID

    Definition VendorIDT :=
      lanarkDottedString.

3
Example vendor ID values include: "com.io7m", "com.example".

## 7.11.12. Version

## 7.11.12.1. Overview

1
The version information for a package is a record consisting of a version number and a version/release date.

### 7.11.12.1.2. Version

    Inductive VersionT := Version {
      versionNumber : VersionNumberT;
      versionDate   : VersionDateT
    }.

## 7.11.12.2. Number

1
The version number is the semantic version of the package.

### 7.11.12.2.2. Version Number

    Inductive VersionNumberT := VersionNumber {
      major     : nat;
      minor     : nat;
      patch     : nat;
      qualifier : option string
    }.

## 7.11.12.3. Date

1
The version date is an ISO 8601 date string denoting the release date of this version of the package.

### 7.11.12.3.2. Version Date

    Inductive VersionDateT :=
      VersionDate : forall (s : string),
        matches s (regex "[0-9]{4}-[0-9]{2}-[0-9]{2}")
          -> VersionDateT.

3
Example version date values include: "2024-10-13", "2001-01-23".

## 7.12. Manifest

## 7.12.1. Overview

1
A manifest consists of a set of items.

### 7.12.1.2. Manifest

    Inductive ManifestT := Manifest {
      manifestItems : list ItemT
    }.

3
An item is a Module, PlatformModule, or a Resource.

### 7.12.1.4. Item

    Inductive ItemT :=
      | ItemModule         : ModuleT         -> ItemT
      | ItemPlatformModule : PlatformModuleT -> ItemT
      | ItemResource       : ResourceT       -> ItemT
      .

5
Items within a manifest must have unique file names. More formally, for a manifest m, there cannot exist two different items i0 and i1 in m such that i0 and i1 have filenames that are the same.

### 7.12.1.6. Manifest File Names

    Definition manifesItemsFilenamesUnique :=
      forall (m : ManifestT),
        forall (i0 : ItemT),
          In i0 (manifestItems m)
            -> ~(exists i1 : ItemT,
                   (In i1 (manifestItems m))
                /\ (i0 <> i1)
                /\ (fileNamesSame (itemFileName i0) (itemFileName i1))).

7
Each item carries a hash value denoting the cryptographic hash of the contents of the item within the package.

## 7.12.2. FileName

1
A file name is a unique name assigned to a manifest item. File names are case-insensitive strings that conform to the regular expression ([\p{L}\p{N}_\-.+]+)(/[\p{L}\p{N}_\-.+]+)*

### 7.12.2.2. FileName

    Inductive FileNameT :=
      FileName : forall (s : string),
        matches s (regex "([\p{L}\p{N}_\-.+]+)(/[\p{L}\p{N}_\-.+]+)*")
          -> FileNameT.

3
Intuitively, a filename can be considered to be a non-empty /-separated list of file name segments that each conform to the regular expression [\p{L}\p{N}_\-.+]+. Accordingly, filenames cannot start with slashes, cannot end with trailing slashes, and cannot contain sequences of repeating slashes.
4
The specification axiomatizes the concept of converting a string to uppercase. The uppercase transform of a string should be understood to be a string where every character has been converted to its uppercase equivalent in a neutral locale.

### 7.12.2.5. Uppercase Transform

    (** A function that produces an uppercase version of the given string. *)
    Parameter uppercaseOf : string -> string.

6
A proposition that states that two strings have the same uppercase transform:

### 7.12.2.7. Uppercase Same

    Definition uppercaseSame (s t : string) :=
      uppercaseOf s = uppercaseOf t.

8
Accordingly, as file names are case-insensitive, then two file names are equal if their uppercase transforms are equal:

### 7.12.2.9. File Names Same

    (** A proposition that states that two file names are the same if their
        uppercase transformations are the same. *)
    Definition fileNamesSame (s t : FileNameT) :=
      match s, t with
      | FileName fs _, FileName ft _ => uppercaseSame fs ft
      end.

## 7.12.3. Size

1
A size is a non-negative integer value denoting the size in octets of an item.

## 7.12.4. Modules

1
A module represents a platform-neutral jar file that will be placed onto the Java module path regardless of the underlying hardware architecture and operating system on which the application is running.

### 7.12.4.2. Module

    Inductive ModuleT := Module {
      mFile : FileNameT;
      mHash : HashT;
      mSize : nat
    }.

## 7.12.5. PlatformModules

1
A platform module represents a platform-specific jar file that will be placed onto the Java module path when the hardware architecture and operating system of the module matches that of the platform upon which the application is running.

### 7.12.5.2. PlatformModule

    Inductive PlatformModuleT := PlatformModule {
      pmFile     : FileNameT;
      pmHash     : HashT;
      pmPlatform : PlatformT;
      pmSize     : nat
    }.

## 7.12.6. Resources

1
A resource is an arbitrary file associated with the package. Resources are typically used to provide icons, BOMs, and screenshots for the package.

### 7.12.6.2. Resource

    Inductive ResourceT := Resource {
      rFile    : FileNameT;
      rHash    : HashT;
      rRole    : ResourceRoleT;
      rCaption : CaptionT;
      rSize    : nat
    }.

3
A resource has an associated role that describes the purpose of the resource.

### 7.12.6.4. Resource Role

    Inductive ResourceRoleT :=
      | BOM
      | LICENSE
      | ICO_WINDOWS
      | ICON_16
      | ICON_24
      | ICON_32
      | ICON_48
      | ICON_64
      | ICON_128
      | ICON_256
      | ICON_512
      | ICON_SVG
      | SCREENSHOT
      .

5
A role has one of the following values:

### 7.12.6.6. Resource Role Values

Value | Description
--- | ---
BOM | A bill-of-materials. Recommended to be in CycloneDX format.
LICENSE | A plain text license file.
ICO_WINDOWS | A Windows application icon (".ico").
ICON_16 | A 16x16 application icon.
ICON_24 | A 24x24 application icon.
ICON_32 | A 32x32 application icon.
ICON_48 | A 48x48 application icon.
ICON_64 | A 64x64 application icon.
ICON_128 | A 128x128 application icon.
ICON_256 | A 256x256 application icon.
ICON_512 | A 512x512 application icon.
ICON_SVG | An arbitrarily scaled SVG icon.
SCREENSHOT | A screenshot.

7
A resource has an associated caption that provides a human-readable description of the resource. This is used, for example, to describe the contents of screenshots for use in Flatpak listings.

### 7.12.6.8. Resource Caption

    Definition CaptionT :=
      TranslatedTextT.

## 7.13. Serialization

## 7.13.1. Overview

1
montarre package declarations are serialized to an XML format with a strict XSD schema. The serialized package declaration, and all the package contents, are collected into binary file format based on the Entomos file format specification. Restrictions are applied to the XML data to assist with ensuring that montarre packages are reproducible.

## 7.13.2. Entomos

1
montarre packages are entomos files with the file extension .mpk.
2
All entomos files have the following structure:

### 7.13.2.3. Entomos Structure

- Files start with a 64-bit format-specific tag for easy identification.
- The file tag is followed by a 32-bit major and minor version.
- The rest of the file is divided into a flat array of sections.
- Each section is aligned to a 16-byte boundary.
- Each section starts with a 64-bit format-specific tag.
- The section tag is followed by a 64-bit size value, specifying the length of the data within the section.
- The section then contains size bytes of data, followed by up to 15 bytes of padding in order to ensure that any data that follows is aligned to a 16-byte boundary.
- The file ends with an end section. This is a normal section where the section has a format-specific end tag, and a size of 0.
- Readers are required to stop reading at the end section. Trailing data is ignored.
- Readers are required to fail if there is no end section, and treat the file as corrupted and truncated.
- All values are in big-endian order. The data within sections can be in any byte order as required by specific formats.

4
The file format is versioned according to the following rules:

### 7.13.2.5. Versioning

- The specification is versioned via a restricted subset of the Semantic Versioning specification. The specification has a major and minor version number, with major version increments denoting incompatible changes, and minor version increments denoting new functionality. There is no patch version number. A version of the specification with major version m and minor version n is denoted as specification version (m, n).
- Assuming a version of the specification m, an update to the specification that yields version n such that n > m is considered to be forwards compatible if a parser that supports format version m can read files that were written using format version n.
- Assuming a version of the specification m, an update to the specification that yields version n such that n > m is considered to be backwards compatible if a parser that supports format version n can read files that were written using format version m.
- The specification is designed such that a correctly-written parser implementation that supports a major version m is able to support the set of versions ∀n. (m, n). This implies full forwards and backwards compatibility for parsers when the major version is unchanged.
- Changes that would cause a parser supporting an older version of the specification to fail to read a file written according to a newer version of the specification MUST imply an increment in the major version of the specification.
- Changes that would cause a parser supporting a newer version of the specification to fail to read a file written according to an older version of the specification MUST imply an increment in the major version of the specification.

6
Every montarre package file starts with the given fixed-size header:

### 7.13.2.7. File Header

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

8
This version of the specification defines major version 1, minor version 0.
9
The package declaration is serialized to XML and stored in the manifest section of the file. There must be exactly one manifest section, and it must be the first section in the file.

### 7.13.2.10. Manifest Section

    Definition binaryManifestSection (m : ManifestT) : binaryExp :=
      let text := utf8 (xmlSerializationOf m) in
        BiRecord [
          ("id",   u64 0x4D54505F4D414E49);
          ("size", u64 (binarySize text));
          ("text", text)
        ].

11
Each file listed in the manifest is stored in its own file section. A file section starts with the name of the file and is followed directly by the file data.

### 7.13.2.12. File Section

    Definition binaryFileSection (i : ItemT) : binaryExp :=
      let nameText  := utf8 (uppercaseOf (fileNameString (itemFileName i))) in
      let nameSize  := binarySize nameText in
      let fileSize  := itemSize i in
      let totalSize := 4 + nameSize + fileSize in
        BiRecord [
          ("id",         u64 0x4D54505F46494C45);
          ("size",       u64 totalSize);
          ("nameLength", u32 nameSize);
          ("name",       nameText);
          ("data",       BiReserve fileSize)
        ].

13
File sections are subject to the following restrictions and observations:

### 7.13.2.14. File Section Restrictions / Observations

- File sections must be serialized such that the names in each section appear in ascending alphabetical order. We specify a serialization order to ensure that implementations produce reproducible files.
- For every file section, there must be a corresponding item declared in the manifest. It is not permitted to place "extra" file sections in the file.
- For every item declared in the manifest, there must be a corresponding file section. It is not permitted to omit file sections.
- The size of the data in a file section is equal to the declared size of the corresponding item in the manifest, minus the length of the UTF-8 encoded file name, and four octets to store the length of the name, and any padding required to align the following section.

15
Every montarre package file ends with an end section.

### 7.13.2.16. End Section

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

## 7.13.3. XML

1
Package declarations must be serialized according to the included schema with the following restrictions:

### 7.13.3.2. XML Restrictions

- XML must be serialized indented to four spaces.
- The character content of elements must be serialized using a function equivalent to XSLT's normalize-space() function.
- After indenting, XML must be canonicalized using the Exclusive XML Canonicalization Version 1.0 algorithm.

## 7.13.4. XML Schema

1
The package declaration schema is as follows:

### 7.13.4.2. XML Schema

    <?xml version="1.0" encoding="UTF-8" ?>

    <xsd:schema xmlns:xsd="http://www.w3.org/2001/XMLSchema"
                targetNamespace="urn:com.io7m.montarre.package:1"
                xmlns:mp="urn:com.io7m.montarre.package:1">

      <xsd:simpleType name="ApplicationKindType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            The type of application. Many packaging systems and some operating systems distinguish between "console" and
            "graphical" applications.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:enumeration value="CONSOLE"/>
          <xsd:enumeration value="GRAPHICAL"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="VersionType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            An arbitrary version number.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string"/>
      </xsd:simpleType>

      <xsd:simpleType name="CategoryNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A category name.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[A-Z][A-Za-z0-9_-]{0,128}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="VendorIDType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A vendor ID; A Lanark dotted name.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="([a-z][a-z0-9_-]{0,63})(\.[a-z][a-z0-9_-]{0,62}){0,15}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="PackageNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A package name; A Lanark dotted name.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="([a-z][a-z0-9_-]{0,63})(\.[a-z][a-z0-9_-]{0,62}){0,15}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="ShortNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A short package name. Used for systems such as Debian packages.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[a-z][a-z0-9_-]{0,128}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="HashAlgorithmNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A hash algorithm name. See " Java Security Standard Algorithm Names".
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[A-Z][A-Z0-9_-]{0,128}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="HashValueType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A hex-encoded hash value.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[a-f0-9]{2,256}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="OSNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            An operating system name.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[a-z][a-z0-9_-]{0,32}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="ArchitectureNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A hardware architecture name.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[a-z][a-z0-9_-]{0,32}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="VendorNameType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A vendor name. Must be a filesystem-safe name as these names can be used as directories in Windows installers.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="[a-zA-Z][A-Za-z0-9_-]{0,128}"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:simpleType name="FlatpakPermissionType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A flatpak permission.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:pattern value="--[a-z\-]+(=[a-zA-Z0-9\\._\-/:~]+)?"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:element name="Version">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            Version information.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:attribute name="Number"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The version number. Typically in semantic version form ("2.0.0", "1.0.0-SNAPSHOT", etc).
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Date"
                         type="xsd:date"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The date the version was set.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Vendor">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A vendor.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:attribute name="ID"
                         type="mp:VendorIDType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The unique vendor ID.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Name"
                         type="mp:VendorNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The vendor name.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Category">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A category applied to an application.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:attribute name="Name"
                         type="mp:CategoryNameType"
                         use="required"/>
        </xsd:complexType>
      </xsd:element>

      <xsd:simpleType name="LinkRole">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            The role of a link.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:enumeration value="ISSUES"/>
          <xsd:enumeration value="HOME_PAGE"/>
          <xsd:enumeration value="DONATION"/>
          <xsd:enumeration value="CONTACT"/>
          <xsd:enumeration value="FAQ"/>
          <xsd:enumeration value="TRANSLATE"/>
          <xsd:enumeration value="CONTRIBUTE"/>
          <xsd:enumeration value="SCM"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:element name="Link">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A link.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:attribute name="Role"
                         type="mp:LinkRole"
                         use="required"/>
          <xsd:attribute name="Target"
                         type="xsd:anyURI"
                         use="required"/>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Copying">
        <xsd:complexType>
          <xsd:attribute name="License"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                An SPDX license identifier such as "ISC".
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Copyright"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                A copyright string such as "Copyright © 2024 Mark Raynsford &lt;code@io7m.com> https://www.io7m.com".
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:simpleType name="RuntimeImageKindType">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            The type of JDK required by the application. Some applications may require a full JDK image with jdk.* modules,
            whereas other applications can work with a reduced JRE image.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:restriction base="xsd:string">
          <xsd:enumeration value="JDK"/>
          <xsd:enumeration value="JRE"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:element name="ExtraOption">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            An extra option passed to the Java runtime.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:attribute name="Value"
                         type="xsd:string"
                         use="required"/>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="EnableNativeAccess">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A Java module name.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:attribute name="Module"
                         type="xsd:string"
                         use="required"/>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="JavaInfo">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            Information relative to the Java runtime.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:sequence minOccurs="0" maxOccurs="unbounded">
            <xsd:choice>
              <xsd:element ref="mp:EnableNativeAccess"/>
              <xsd:element ref="mp:ExtraOption"/>
            </xsd:choice>
          </xsd:sequence>

          <xsd:attribute name="RequiredJDKVersion"
                         type="xsd:unsignedLong"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The required JDK version.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="RuntimeImageKind"
                         type="mp:RuntimeImageKindType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The required JDK runtime kind.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="MainModule"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The main application module. This should be in a fully-qualified module form such as
                "com.io7m.montarre.cmdline/com.io7m.montarre.cmdline.MMain".
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Names">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            Package name information.
          </xsd:documentation>
        </xsd:annotation>
        <xsd:complexType>
          <xsd:attribute name="Name"
                         type="mp:PackageNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The package name.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="ShortName"
                         type="mp:ShortNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The package short name. The short name is used when exporting to some native package systems such as Debian
                packages.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HumanName"
                         type="xsd:string"
                         use="optional">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The optional human-readable application name. This will default to the package name if not specified.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:simpleType name="FlatpakRuntimeRole">
        <xsd:restriction base="xsd:string">
          <xsd:enumeration value="PLATFORM"/>
          <xsd:enumeration value="SDK"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:element name="FlatpakPermission">
        <xsd:complexType>
          <xsd:attribute name="Value"
                         use="required"
                         type="mp:FlatpakPermissionType">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                A flatpak permission such as "--share=network", "--share=ipc", etc.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="FlatpakRuntime">
        <xsd:complexType>
          <xsd:attribute name="Name"
                         use="required"
                         type="xsd:string">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                A flatpak runtime such as "org.freedesktop.Platform".
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Version"
                         use="required"
                         type="xsd:string">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                A flatpak runtime version such as "24.08".
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Role"
                         use="required"
                         type="mp:FlatpakRuntimeRole">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                A runtime role such as "PLATFORM" or "SDK".
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Flatpak">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            Metadata specific to Flatpak packages.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType>
          <xsd:sequence>
            <xsd:sequence minOccurs="0"
                          maxOccurs="unbounded">
              <xsd:element ref="mp:FlatpakPermission"/>
            </xsd:sequence>
            <xsd:sequence minOccurs="0"
                          maxOccurs="unbounded">
              <xsd:element ref="mp:FlatpakRuntime"/>
            </xsd:sequence>
          </xsd:sequence>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Text">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A text element in a specific language.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType mixed="true">
          <xsd:attribute name="Language"
                         use="required"
                         type="xsd:NMTOKEN"/>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Description">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A humanly-readable package description.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType>
          <xsd:sequence minOccurs="0"
                        maxOccurs="1">
            <xsd:element ref="mp:Text"/>
          </xsd:sequence>
        </xsd:complexType>

        <xsd:unique name="DescriptionTextLanguageUnique">
          <xsd:selector xpath="mp:Text"/>
          <xsd:field xpath="@Language"/>
        </xsd:unique>
      </xsd:element>

      <xsd:element name="Feature">
        <xsd:complexType mixed="true"/>
      </xsd:element>

      <xsd:element name="Paragraph">
        <xsd:complexType mixed="true"/>
      </xsd:element>

      <xsd:element name="LongDescription">
        <xsd:complexType>
          <xsd:sequence>
            <xsd:sequence minOccurs="1"
                          maxOccurs="unbounded">
              <xsd:element ref="mp:Paragraph"/>
            </xsd:sequence>
            <xsd:sequence minOccurs="0"
                          maxOccurs="unbounded">
              <xsd:element ref="mp:Feature"/>
            </xsd:sequence>
          </xsd:sequence>

          <xsd:attribute name="Language"
                         use="required"
                         type="xsd:NMTOKEN"/>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Caption">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A humanly-readable resource caption.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType>
          <xsd:sequence minOccurs="1"
                        maxOccurs="unbounded">
            <xsd:element ref="mp:Text"/>
          </xsd:sequence>
        </xsd:complexType>

        <xsd:unique name="CaptionTextLanguageUnique">
          <xsd:selector xpath="mp:Text"/>
          <xsd:field xpath="@Language"/>
        </xsd:unique>
      </xsd:element>

      <xsd:element name="Metadata">
        <xsd:complexType>
          <xsd:sequence>
            <xsd:sequence minOccurs="0"
                          maxOccurs="unbounded">
              <xsd:element ref="mp:Category"/>
            </xsd:sequence>
            <xsd:element ref="mp:Copying"/>
            <xsd:element ref="mp:Description"/>
            <xsd:sequence>
              <xsd:element ref="mp:Flatpak"
                           minOccurs="0"
                           maxOccurs="1"/>
            </xsd:sequence>
            <xsd:element ref="mp:JavaInfo"/>
            <xsd:sequence minOccurs="0"
                          maxOccurs="unbounded">
              <xsd:element ref="mp:Link"/>
            </xsd:sequence>
            <xsd:sequence minOccurs="0"
                          maxOccurs="1">
              <xsd:element ref="mp:LongDescription"/>
            </xsd:sequence>
            <xsd:element ref="mp:Names"/>
            <xsd:element ref="mp:Vendor"/>
            <xsd:element ref="mp:Version"/>
          </xsd:sequence>

          <xsd:attribute name="ApplicationKind"
                         type="mp:ApplicationKindType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The kind of the application.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="PlatformDependentModule">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A module that is only used when running on a specific platform.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType>
          <xsd:attribute name="File"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file name within the package.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Size"
                         type="xsd:unsignedLong"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The size of the file in octets.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HashAlgorithm"
                         type="mp:HashAlgorithmNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file hash algorithm name.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HashValue"
                         type="mp:HashValueType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file hash value.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="OperatingSystem"
                         type="mp:OSNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The operating system on which this module is used.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Architecture"
                         type="mp:ArchitectureNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The hardware architecture on which this module is used.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:element name="Module">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A module that is used on all platforms.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType>
          <xsd:attribute name="File"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file name within the package.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Size"
                         type="xsd:unsignedLong"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The size of the file in octets.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HashAlgorithm"
                         type="mp:HashAlgorithmNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file hash algorithm name.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HashValue"
                         type="mp:HashValueType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file hash value.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:simpleType name="ResourceRole">
        <xsd:restriction base="xsd:string">
          <xsd:enumeration value="BOM"/>
          <xsd:enumeration value="ICON_128"/>
          <xsd:enumeration value="ICON_16"/>
          <xsd:enumeration value="ICON_24"/>
          <xsd:enumeration value="ICON_256"/>
          <xsd:enumeration value="ICON_32"/>
          <xsd:enumeration value="ICON_48"/>
          <xsd:enumeration value="ICON_64"/>
          <xsd:enumeration value="ICO_WINDOWS"/>
          <xsd:enumeration value="LICENSE"/>
          <xsd:enumeration value="SCREENSHOT"/>
        </xsd:restriction>
      </xsd:simpleType>

      <xsd:element name="Resource">
        <xsd:annotation>
          <xsd:documentation xml:lang="en">
            A metadata resource.
          </xsd:documentation>
        </xsd:annotation>

        <xsd:complexType>
          <xsd:sequence>
            <xsd:element ref="mp:Caption"
                         minOccurs="0"
                         maxOccurs="1"/>
          </xsd:sequence>

          <xsd:attribute name="File"
                         type="xsd:string"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file name within the package.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Size"
                         type="xsd:unsignedLong"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The size of the file in octets.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HashAlgorithm"
                         type="mp:HashAlgorithmNameType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file hash algorithm name.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="HashValue"
                         type="mp:HashValueType"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The file hash value.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
          <xsd:attribute name="Role"
                         type="mp:ResourceRole"
                         use="required">
            <xsd:annotation>
              <xsd:documentation xml:lang="en">
                The role of the resource.
              </xsd:documentation>
            </xsd:annotation>
          </xsd:attribute>
        </xsd:complexType>
      </xsd:element>

      <xsd:group name="ManifestItemGroup">
        <xsd:choice>
          <xsd:element ref="mp:Module"/>
          <xsd:element ref="mp:PlatformDependentModule"/>
          <xsd:element ref="mp:Resource"/>
        </xsd:choice>
      </xsd:group>

      <xsd:element name="Manifest">
        <xsd:complexType>
          <xsd:sequence minOccurs="0"
                        maxOccurs="unbounded">
            <xsd:group ref="mp:ManifestItemGroup"/>
          </xsd:sequence>
        </xsd:complexType>

        <xsd:key name="ManifestItemUnique">
          <xsd:selector xpath="mp:Module|mp:PlatformDependentModule|mp:BOM"/>
          <xsd:field xpath="@File"/>
        </xsd:key>
      </xsd:element>

      <xsd:element name="Package">
        <xsd:complexType>
          <xsd:sequence>
            <xsd:element ref="mp:Metadata"/>
            <xsd:element ref="mp:Manifest"/>
          </xsd:sequence>
        </xsd:complexType>
      </xsd:element>

    </xsd:schema>

## 7.14. Model Sources

1
The full sources of the specification model are provided here.

### 7.14.2. Montarre/Package.v

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

    From Stdlib Require Import Strings.String.
    From Stdlib Require Import Strings.Ascii.
    From Stdlib Require Import FSets.FMapInterface.
    From Stdlib Require Import FSets.FMapWeakList.
    From Stdlib Require Import FSets.FMapFacts.
    From Stdlib Require Import Structures.Equalities.

    Require Import com.io7m.entomos.Binary.

    Import ListNotations.
    Local Open Scope string_scope.

    (** A mini decidable type module to instantiate maps. *)
    Module StringMiniDec : MiniDecidableType
      with Definition t := string.

      Definition t        := string.
      Definition eq       := @Logic.eq t.
      Definition eq_refl  := @Logic.eq_refl t.
      Definition eq_sym   := @Logic.eq_sym t.
      Definition eq_trans := @Logic.eq_trans t.

      Theorem eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
      Proof. apply string_dec. Qed.
    End StringMiniDec.

    (** A usual decidable type module to instantiate maps. *)
    Module StringDec <: UsualDecidableType
      with Definition t := string
      with Definition eq := @Logic.eq string
    := Make_UDT StringMiniDec.

    (** A Maps module with string keys. *)
    Module StringMaps : FMapInterface.WS
      with Definition E.t  := string
      with Definition E.eq := @Logic.eq string
    := FMapWeakList.Make StringDec.

    (** The opaque, abstract type of regular expressions. *)
    Parameter RegularExpressionT : string -> Set.

    (** For the sake of specification simplicity, we assume that all
        strings are valid regular expressions. *)
    Parameter regex : forall (s : string), RegularExpressionT s.

    (** A proposition that states that a given regular expression
        matches a given string. *)
    Parameter matches : forall (s : string) {e : string},
      RegularExpressionT e -> Prop.

    (** Whether a string matches a regular expression is decidable. *)
    Parameter matchesDecidable : forall
      (s : string)
      {e : string}
      (r : RegularExpressionT e),
        {matches s r}+{~matches s r}.

    Definition lanarkDottedString :=
      forall (s : string),
        matches s (regex "([a-z][a-z0-9_-]{0,63})(\.[a-z][a-z0-9_-]{0,62}){0,15}").

    Inductive ApplicationKindT :=
      | CONSOLE
      | GRAPHICAL
      .

    Inductive CategoryT :=
      Category : forall (s : string),
        matches s (regex "[A-Z][A-Za-z0-9_-]{0,128}")
          -> CategoryT.

    Definition LicenseT :=
      string.

    Definition CopyrightT :=
      string.

    Inductive CopyingT := Copying {
      license   : LicenseT;
      copyright : CopyrightT
    }.

    Definition LanguageT :=
      string.

    (** A Maps module with language keys. *)
    Module LanguageMaps : FMapInterface.WS
      with Definition E.t  := LanguageT
      with Definition E.eq := @Logic.eq LanguageT
    := FMapWeakList.Make StringDec.

    Inductive TranslatedTextT := TranslatedText {
      language     : LanguageT;
      text         : string;
      translations : LanguageMaps.t string
    }.

    Definition DescriptionT :=
      TranslatedTextT.

    Inductive JavaImageT :=
        JDK
      | JRE.

    Inductive JavaInfoT := JavaInfo {
      requiredJDKVersion : nat;
      mainModule         : string;
      extraOptions       : list string;
      enableNativeAccess : list string;
      imageType          : JavaImageT
    }.

    Inductive LinkRoleT :=
      | ISSUES
      | HOME_PAGE
      | DONATION
      | CONTACT
      | FAQ
      | TRANSLATE
      | CONTRIBUTE
      | SCM
      .

    Inductive LinkT := Link {
      linkRole   : LinkRoleT;
      linkTarget : string
    }.

    Inductive VendorNameT :=
      VendorName : forall (s : string),
        matches s (regex "[a-zA-Z][A-Za-z0-9_-]{0,128}")
          -> VendorNameT.

    Definition VendorIDT :=
      lanarkDottedString.

    Inductive VendorT := Vendor {
      vendorId   : VendorIDT;
      vendorName : VendorNameT
    }.

    Inductive VersionNumberT := VersionNumber {
      major     : nat;
      minor     : nat;
      patch     : nat;
      qualifier : option string
    }.

    Inductive VersionDateT :=
      VersionDate : forall (s : string),
        matches s (regex "[0-9]{4}-[0-9]{2}-[0-9]{2}")
          -> VersionDateT.

    Inductive VersionT := Version {
      versionNumber : VersionNumberT;
      versionDate   : VersionDateT
    }.

    Definition ParagraphT :=
      string.

    Definition FeatureT :=
      string.

    Inductive LongDescriptionT := LongDescription {
      descriptionLanguage : LanguageT;
      descriptions        : list ParagraphT;
      features            : list FeatureT
    }.

    Inductive FlatpakRuntimeRoleT :=
      | SDK
      | PLATFORM
      .

    Definition FlatpakPermissionT :=
      string.

    Inductive FlatpakRuntimeT := FlatpakRuntime {
      flatpakRuntimeName    : string;
      flatpakRuntimeVersion : string;
      flatpakRuntimeRole    : FlatpakRuntimeRoleT
    }.

    Inductive FlatpakT := Flatpak {
      flatpakPermissions : list FlatpakPermissionT;
      flatpakRuntimes    : list FlatpakRuntimeT
    }.

    Definition PackageNameT :=
      lanarkDottedString.

    Inductive ShortNameT :=
      ShortName : forall (s : string),
        matches s (regex "[a-z][a-z0-9_-]{0,128}")
          -> ShortNameT.

    Definition HumanNameT :=
      string.

    Inductive NamesT := Names {
      namePackage : PackageNameT;
      nameShort   : ShortNameT;
      nameHuman   : HumanNameT
    }.

    Inductive MetadataT := Metadata {
      metaApplicationKind  : ApplicationKindT;
      metaCategories       : list CategoryT;
      metaCopying          : CopyingT;
      metaDescription      : DescriptionT;
      metaFlatpak          : FlatpakT;
      metaJavaInfo         : JavaInfoT;
      metaLinks            : list LinkT;
      metaLongDescriptions : LanguageMaps.t LongDescriptionT;
      metaNames            : NamesT;
      metaVendor           : VendorT;
      metaVersion          : VersionT
    }.

    Definition HashAlgorithmT :=
      string.

    Inductive HashValueT :=
      HashValue : forall (s : string),
        matches s (regex "[a-f0-9]{2,256}")
          -> HashValueT.

    Inductive HashT := Hash {
      hashAlgorithm : HashAlgorithmT;
      hashValue     : HashValueT
    }.

    Inductive ArchitectureNameT :=
      ArchitectureName : forall (s : string),
        matches s (regex "[a-z][a-z0-9_-]{0,32}")
          -> ArchitectureNameT.

    Inductive OperatingSystemNameT :=
      OperatingSystemName : forall (s : string),
        matches s (regex "[a-z][a-z0-9_-]{0,32}")
          -> OperatingSystemNameT.

    Inductive PlatformT := Platform {
      platformArch : ArchitectureNameT;
      platformOS   : OperatingSystemNameT
    }.

    (** A function that produces an uppercase version of the given string. *)
    Parameter uppercaseOf : string -> string.

    Definition uppercaseSame (s t : string) :=
      uppercaseOf s = uppercaseOf t.

    Inductive FileNameT :=
      FileName : forall (s : string),
        matches s (regex "([\p{L}\p{N}_\-.+]+)(/[\p{L}\p{N}_\-.+]+)*")
          -> FileNameT.

    Definition fileNameString (i : FileNameT) : string :=
      match i with
      | FileName s _ => s
      end.

    (** A proposition that states that two file names are the same if their
        uppercase transformations are the same. *)
    Definition fileNamesSame (s t : FileNameT) :=
      match s, t with
      | FileName fs _, FileName ft _ => uppercaseSame fs ft
      end.

    Inductive ResourceRoleT :=
      | BOM
      | LICENSE
      | ICO_WINDOWS
      | ICON_16
      | ICON_24
      | ICON_32
      | ICON_48
      | ICON_64
      | ICON_128
      | ICON_256
      | ICON_512
      | ICON_SVG
      | SCREENSHOT
      .

    Definition CaptionT :=
      TranslatedTextT.

    Inductive ModuleT := Module {
      mFile : FileNameT;
      mHash : HashT;
      mSize : nat
    }.

    Inductive PlatformModuleT := PlatformModule {
      pmFile     : FileNameT;
      pmHash     : HashT;
      pmPlatform : PlatformT;
      pmSize     : nat
    }.

    Inductive ResourceT := Resource {
      rFile    : FileNameT;
      rHash    : HashT;
      rRole    : ResourceRoleT;
      rCaption : CaptionT;
      rSize    : nat
    }.

    Inductive ItemT :=
      | ItemModule         : ModuleT         -> ItemT
      | ItemPlatformModule : PlatformModuleT -> ItemT
      | ItemResource       : ResourceT       -> ItemT
      .

    Definition itemFileName (i : ItemT) : FileNameT :=
      match i with
      | ItemModule         x => mFile x
      | ItemPlatformModule x => pmFile x
      | ItemResource       x => rFile x
      end.

    Definition itemHash (i : ItemT) : HashT :=
      match i with
      | ItemModule         x => mHash x
      | ItemPlatformModule x => pmHash x
      | ItemResource       x => rHash x
      end.

    Definition itemSize (i : ItemT) : nat :=
      match i with
      | ItemModule         x => mSize x
      | ItemPlatformModule x => pmSize x
      | ItemResource       x => rSize x
      end.

    Inductive ManifestT := Manifest {
      manifestItems : list ItemT
    }.

    Definition manifesItemsFilenamesUnique :=
      forall (m : ManifestT),
        forall (i0 : ItemT),
          In i0 (manifestItems m)
            -> ~(exists i1 : ItemT,
                   (In i1 (manifestItems m))
                /\ (i0 <> i1)
                /\ (fileNamesSame (itemFileName i0) (itemFileName i1))).

    (** A function that produces an XML serialization of the given manifest. *)
    Parameter xmlSerializationOf : ManifestT -> string.

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

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

    (** The MTP_MANI section. *)
    Definition binaryManifestSection (m : ManifestT) : binaryExp :=
      let text := utf8 (xmlSerializationOf m) in
        BiRecord [
          ("id",   u64 0x4D54505F4D414E49);
          ("size", u64 (binarySize text));
          ("text", text)
        ].

    (** The MTP_FILE section. *)
    Definition binaryFileSection (i : ItemT) : binaryExp :=
      let nameText  := utf8 (uppercaseOf (fileNameString (itemFileName i))) in
      let nameSize  := binarySize nameText in
      let fileSize  := itemSize i in
      let totalSize := 4 + nameSize + fileSize in
        BiRecord [
          ("id",         u64 0x4D54505F46494C45);
          ("size",       u64 totalSize);
          ("nameLength", u32 nameSize);
          ("name",       nameText);
          ("data",       BiReserve fileSize)
        ].

## Footnotes

1 | Vendor names are used in some native packaging systems as installation directories and are therefore required to be filesystem-safe. References to this footnote: 1
2 | Short names are used in some native packaging systems as executable names and are therefore required to be filesystem-safe. References to this footnote: 1
3 | Many hardware architectures have different names referring to the same thing. For example, 64-bit x86 hardware is often referred to as amd64, x64, x86_64, etc. References to this footnote: 1

6.5. com.io7m.montarre.shell
Previous
Front Matter
Up
Front Matter
Next
io7m | single-page | multi-page | Montarre User Manual 1.0.0-SNAPSHOT