Initial commit

.gitignore

@@ -0,0 +1,2 @@
+/build
+/build2

README.md

@@ -0,0 +1,89 @@
+# Binman
+
+- Manifests are descriptions of system files
+- Compositions are a system's configuration
+
+Commands:
+
+- `binman check current` checks the integrity of system files against the current manifests
+- `binman check latest` checks the integrity of system files against the latest manifests
+- `binman repair` restore any files that fail an integrity check against a current manifest.
+- `binman refresh` downloads latest manifests
+- `binman apply` applies latest manifests
+- `binman license <path>` prints the license information for a particular file path if the file was installed by binman and the information is available
+- `binman source <path>` downloads the source package associated with a path if the file was installed by binman and a source package is available
+
+File structure
+
+- `/etc/composition` binman composition for this system
+- `/var/binman` directory for manifests and their blobs
+- `/var/binman/base-system` directory for base-system manifest (for example)
+- `/var/binman/base-system/0` manifest with serial 0
+- `/var/binman/base-system/1` manifest with serial 1
+- `/var/binman/base-system/3` manifest with serial 3...
+- `/var/binman/base-system/latest` symbolic link to latest cached manifest
+- `/var/binman/base-system/current` symbolic link to the last applied manifest
+- `/var/binman/base-system/previous` symbolic link to the previously applied manifest
+- `/var/binman/base-system/blob` directory containing any `content` blobs downloaded
+- `/var/binman/base-system/blob/yKwwfp7AeSqgvdX2ZoiB0Qp3IxFEAT0SeMvIJChXBzMNrOvVcQhl9G6ZaHdzPEAe6FTy8shm27ZkDkfaQoMA0g==` bash, as in below example. Reflink copied from here to `/bin/bash` on application.
+
+## Manifest
+
+First entry is header, subsequent entries are files, last entry is signature. `post-exec` is run after the changes are applied. `target` applies only to symlinks. Entire file is xz compressed. `ccs` is the corresponding source code package, and `bin` is the binary file to install - both are technically optional and can be set to `null`. `mod` is the `mode_t` of the file to be created in decimal form.
+
+```jsonl
+{
+    "name": "base-system",
+    "desc": "Base operating system",
+    "serial": 0
+    "post-exec": "/bin/os-setup",
+    "key": "Vm10OzcoMHsneDl2Rm1kbjd3b19QNEpeOF5dIV5Wdmt3fng=",
+    "remotes": [
+        "ipfs://QmPRHT1b8DA1NHJRrYy77yx9jrSiRbxkH82quqonfkiLn3/base-system/",
+        "https://download.astrologue.nz/binaries/base-system/"
+    ],
+}
+{
+    "path": "/bin/bash",
+    "uid": 0,
+    "gid": 0,
+    "mod": 33261,
+    "target": null,
+    "licence": "/usr/share/common-licenses/GPL-3",
+    "bin": {
+        "checksum": "yKwwfp7AeSqgvdX2ZoiB0Qp3IxFEAT0SeMvIJChXBzMNrOvVcQhl9G6ZaHdzPEAe6FTy8shm27ZkDkfaQoMA0g==",
+        "size": 1740896,
+        "remote-path": "0/bin/bash"
+    },
+    "ccs": {
+        "checksum": "akcwfp7AeSqgvdX2ZoiB0Qp3IxFEAT0SeMvIJChXBzMNrOvkk8iosG6ZaHdzPEAe6FTy8shm27ZkDkz8j4mA0a==",
+        "size": 482734,
+        "remote-path": "0/bash-source.tar.xz",
+    }
+}
+{
+    "signature": "0VPgiGlMCqNUgAaNcBZDXxA0ASBMql0mprScGPFXfNN8z9nTcuABMFO594TqNyA41idphV+Qb9yqmhw9WYeiSw==",
+}
+```
+
+
+## Composition
+
+```jsonl
+{
+    "name": "base-system",
+    "key": "Vm10OzcoMHsneDl2Rm1kbjd3b19QNEpeOF5dIV5Wdmt3fng=",
+    "uris": [
+        "ipfs://QmPRHT1b8DA1NHJRrYy77yx9jrSiRbxkH82quqonfkiLn3/base-system.manifest.xz",
+        "https://download.astrologue.nz/binaries/base-system.manifest.xz"
+    ],
+}
+{
+    "name": "gnome-desktop",
+    "key": "Vm10OzcoMHsneDl2Rm1kbjd3b19QNEpeOF5dIV5Wdmt3fng=",
+    "uris": [
+        "ipfs://QmPRHT1b8DA1NHJRrYy77yx9jrSiRbxkH82quqonfkiLn3/gnome-desktop.manifest.xz",
+        "https://download.astrologue.nz/binaries/gnome-desktop.manifest.xz"
+    ],
+}
+```

scripts/acquire.sh

@@ -0,0 +1,7 @@
+#!/bin/bash
+set -e
+
+git init
+git remote add origin https://git.sr.ht/~tilo15/usm || echo "Origin already exists"
+git fetch
+git reset --hard origin/master

scripts/build.sh

@@ -0,0 +1,11 @@
+#!/bin/bash
+set -e
+
+src_dir=$(pwd)
+build_dir=$1
+
+cd ${build_dir}
+
+meson setup ${src_dir}/src --prefix=${PREFIX} --libdir=${LIBDIR} --bindir=${BINDIR} --includedir=${INCLUDEDIR}
+ninja
+

scripts/install.sh

@@ -0,0 +1,10 @@
+#!/bin/bash
+set -e
+
+src_dir=$(pwd)
+build_dir=$1
+install_dir=$2
+
+cd ${build_dir}
+
+meson install --destdir ${install_dir}

src/lib/Applicator.vala

@@ -0,0 +1,132 @@
+using Invercargill;
+namespace Binman {
+
+    public class Applicator {
+
+        public Enumerable<CompositionComponent> composition { get; private set; }
+        public ApplicationType application_type { get; private set; }
+
+        private Enumerable<ManifestFile> manifests;
+        private Dictionary<string, ManifestFile> path_ownership;
+
+        public Applicator(ApplicationType application_type, Enumerable<CompositionComponent>? composition = null) throws Error {
+            this.application_type = application_type;
+            if(composition == null) {
+                this.composition = get_composition().to_series();
+            }
+            else {
+                this.composition = composition.to_series();
+            }
+
+            manifests = composition
+                .try_select<ManifestFile>(c => new ManifestFile.from_name(c.name, application_type, c.key))
+                .to_series();
+
+            path_ownership = new Dictionary<string, ManifestFile>();
+            foreach (var manifest in manifests) {
+                foreach (var entry in manifest.get_entries()) {
+                    path_ownership[entry.unwrap().path] = manifest;
+                }
+            }
+        }
+
+        public void apply() {
+            
+        }
+
+        public Dictionary<string, FileStatus> check_files() throws Error {
+            return manifests
+                .try_select_nested<ManifestEntry>(m => m.get_entries().where(e => path_ownership.get_or_default(e.path) == m))
+                .select_to_dictionary<string, FileStatus>(e => e.path, e => check_installed_file(e));
+        }
+
+        public FileStatus check_installed_file(ManifestEntry entry) {
+            Posix.Stat stat_info;
+            if(Posix.stat(entry.path, out stat_info) != 0) {
+                return FileStatus.MISSING;
+            }
+
+            var status = FileStatus.GOOD;
+            if(stat_info.st_uid != entry.user){
+                status |= FileStatus.BAD_OWNER;
+            }
+            if(stat_info.st_gid != entry.group){
+                status |= FileStatus.BAD_OWNER;
+            }
+
+            if(stat_info.st_mode != entry.mode){
+                status |= FileStatus.BAD_MODE;
+            }
+            else if(Posix.S_ISLNK(entry.mode)) {
+                var buffer = new char[uint16.MAX];
+                buffer.length = (int)Posix.readlink(entry.path, buffer);
+                var target = (string)buffer;
+                if(target != entry.target) {
+                    status |= FileStatus.BAD_CONTENT;
+                }
+            }
+            else if(Posix.S_ISREG(entry.mode) && entry.binary != null) {
+                try {
+                    if(stat_info.st_size != entry.binary.size) {
+                        status |= FileStatus.BAD_CONTENT;
+                    }
+                    else if(!calculate_file_checksum(entry.path).equals(entry.binary.checksum)) {
+                        status |= FileStatus.BAD_CONTENT;
+                    }
+                }
+                catch (Error e) {
+                    warning("Encountered error while calculating file checksum: " + e.message);
+                    status |= FileStatus.BAD_CONTENT;
+                }
+            }
+
+            return status;
+        }
+
+        public BinaryData calculate_file_checksum(string path) throws Error {
+            var stream = File.new_for_path(path).read();
+            var checksum = new Checksum(ChecksumType.SHA512);
+
+            const int increment = 1024 * 1024 * 128;
+            uint64 read = 0;
+            var to_read = stream.query_info("*").get_size();
+            while(read < to_read) {
+                var data = new uint8[uint64.min(increment, to_read - read)];
+                data.length = (int)stream.read(data);
+                checksum.update(data, data.length);
+                read += data.length;
+            }
+
+            var checksum_bytes = new uint8[ChecksumType.SHA512.get_length()];
+            size_t size = checksum_bytes.length;
+            checksum.get_digest(checksum_bytes, ref size);
+
+            return new Invercargill.BinaryData.from_byte_array(checksum_bytes);
+        }
+
+    }
+
+    public enum ApplicationType {
+        CURRENT,
+        LATEST,
+        PREVIOUS;
+
+        public static Mapper<ApplicationType, string> get_mapper() {
+            return ValueMapper.build_for<ApplicationType, string>(cfg => cfg
+                .map(ApplicationType.CURRENT, "current")
+                .map(ApplicationType.LATEST, "latest")
+                .map(ApplicationType.PREVIOUS, "previous")
+            );
+        }
+    }
+
+    [Flags]
+    public enum FileStatus {
+        GOOD = 0,
+        MISSING = (1 << 1),
+        BAD_OWNER = (1 << 2),
+        BAD_GROUP = (1 << 3),
+        BAD_MODE = (1 << 4),
+        BAD_CONTENT = (1 << 5),
+    }
+}

src/lib/Composition.vala

@@ -0,0 +1,27 @@
+using Invercargill;
+using InvercargillJson;
+
+namespace Binman {
+
+    public Attempts<CompositionComponent> get_composition(string path = "/etc/composition") throws Error {
+        return new JsonlInputStream(File.new_for_path(path).read())
+            .as_property_groups()
+            .try_map_with<CompositionComponent>(CompositionComponent.get_mapper());
+    }
+
+    public class CompositionComponent {
+        public string name { get; set; }
+        public BinaryData key { get; set; }
+        public Vector<string> uris { get; set; }
+
+        public static PropertyMapper<CompositionComponent> get_mapper() {
+            return PropertyMapper.build_for<CompositionComponent>(cfg => cfg
+                .map<string>("name", o => o.name, (o, v) => o.name = v)
+                .map<string>("key", o => o.key.to_base64(), (o, v) => o.key = new BinaryData.from_base64(v))
+                .map_many<string>("uris", o => o.uris, (o, v) => o.uris.to_vector())
+                .set_constructor(() => new CompositionComponent())
+            );
+        }
+    }
+
+}

src/lib/Manifest.vala

@@ -0,0 +1,122 @@
+using Invercargill;
+using InvercargillJson;
+
+namespace Binman {
+
+    public errordomain ManifestError {
+        KEY_MISMATCH
+    }
+
+    public class ManifestFile {
+        public File file { get; private set; }
+        
+        public ManifestHeader read_header() throws Error {
+            return new JsonlInputStream(file.read())
+                .as_property_groups()
+                .try_map_with<ManifestHeader>(ManifestHeader.get_mapper())
+                .first()
+                .unwrap();
+        }
+
+        public Attempts<ManifestEntry> get_entries() throws Error {
+            return new JsonlInputStream(file.read())
+                .as_property_groups()
+                .skip(1)
+                .until(o => o.has("signature"))
+                .try_map_with<ManifestEntry>(ManifestEntry.get_mapper());
+        }
+
+        //  public bool verify_signature() throws Error {
+        //      var stream = new DataInputStream(file.read());
+        //      var checksum
+        //  }
+
+        public ManifestFile(File file) {
+            this.file = file;
+        }
+
+        public ManifestFile.from_name(string name, ApplicationType type, BinaryData? key = null) throws Error {
+            this.file = File.new_build_filename("/var/binman", name, ApplicationType.get_mapper().map_from(type));
+            if(!this.file.query_exists()) {
+                throw new FileError.NOENT("Could not find the specified manifest");
+            }
+
+            if(key != null && !read_header().key.equals(key)) {
+                throw new ManifestError.KEY_MISMATCH("The key in the manifest file does not match the key expected");
+            }
+        }
+
+    }
+
+    public class ManifestHeader {
+        public string name { get; set; }
+        public string description { get; set; }
+        public int serial { get; set; }
+        public string post_exec { get; set; }
+        public BinaryData key { get; set; }
+        public Vector<string> remotes { get; set; }
+
+        public static PropertyMapper<ManifestHeader> get_mapper() {
+            return PropertyMapper.build_for<ManifestHeader>(cfg => {
+                cfg.map<string>("name", o => o.name, (o, v) => o.name = v);
+                cfg.map<string>("desc", o => o.description, (o, v) => o.description = v);
+                cfg.map<int>("serial", o => o.serial, (o, v) => o.serial = v);
+                cfg.map<string>("post-exec", o => o.post_exec, (o, v) => o.post_exec = v);
+                cfg.map<string>("key", o => o.key.to_base64(), (o, v) => o.key = new BinaryData.from_base64(v));
+                cfg.map_many<string>("remotes", o => o.remotes, (o, v) => o.remotes = v.to_vector());
+                cfg.set_constructor(() => new ManifestHeader());
+            });
+        }
+    }
+
+    public class ManifestEntry {
+        public string path { get; set; }
+        public int user { get; set; }
+        public int group { get; set; }
+        public Posix.mode_t mode { get; set; }
+        public string? target { get; set; }
+        public string? licence { get; set; }
+        public ManifestFileDescriptor? binary { get; set; }
+        public ManifestFileDescriptor? source { get; set; }
+
+        public static PropertyMapper<ManifestEntry> get_mapper() {
+            return PropertyMapper.build_for<ManifestEntry>(cfg => cfg
+                .map<string>("path", o => o.path, (o, v) => o.path = v)
+                .map<int>("uid", o => o.user, (o, v) => o.user = v)
+                .map<int>("gid", o => o.group, (o, v) => o.group = v)
+                .map<int>("mod", o => (int)o.mode, (o, v) => o.mode = v)
+                .map<string?>("target", o => o.target, (o, v) => o.target = v, false)
+                .map<string?>("licence", o => o.licence, (o, v) => o.licence = v, false)
+                .map_properties_with<ManifestFileDescriptor?>("bin", o => o.binary, (o, v) => o.binary = v, ManifestFileDescriptor.get_mapper(), false)
+                .map_properties_with<ManifestFileDescriptor?>("ccs", o => o.source, (o, v) => o.source = v, ManifestFileDescriptor.get_mapper(), false)
+                .set_constructor(() => new ManifestEntry())
+            );
+        }
+    }
+
+    public class ManifestFileDescriptor {
+        public BinaryData checksum { get; set; }
+        public uint64 size { get; set; }
+        public string remote_path { get; set; }
+
+        public static PropertyMapper<ManifestFileDescriptor> get_mapper() {
+            return PropertyMapper.build_for<ManifestFileDescriptor>(cfg => cfg
+                .map<string>("checksum", o => o.checksum.to_base64(), (o, v) => o.checksum = new BinaryData.from_base64(v))
+                .map<uint64?>("size", o => o.size, (o, v) => o.size = v)
+                .map<string>("path", o => o.remote_path, (o, v) => o.remote_path = v)
+                .set_constructor(() => new ManifestFileDescriptor())
+            );
+        }
+    }
+
+    public class ManifestSignature {
+        public BinaryData signature { get; set; }
+
+        public static PropertyMapper<ManifestSignature> get_mapper() {
+            return PropertyMapper.build_for<ManifestSignature>(cfg => cfg
+                .map<string>("signature", o => o.signature.to_base64(), (o, v) => o.signature = new BinaryData.from_base64(v))
+                .set_constructor(() => new ManifestSignature())
+            );
+        }
+    }
+}

src/lib/meson.build

@@ -0,0 +1,43 @@
+
+add_project_arguments(['--debug', '--disable-warnings', '--enable-checking','--vapidir', vapi_dir], language: 'vala')
+
+sources = files('Manifest.vala')
+sources += files('Composition.vala')
+sources += files('Applicator.vala')
+sources += files('ManifestUpdater.vala')
+sources += files('BlobStorage.vala')
+
+
+dependencies = [
+    dependency('glib-2.0'),
+    dependency('gobject-2.0'),
+    dependency('gio-2.0'),
+    dependency('gee-0.8'),
+    dependency('json-glib-1.0'),
+    dependency('invercargill'),
+    dependency('invercargill-json'),
+    meson.get_compiler('vala').find_library('posix'),
+    meson.get_compiler('vala').find_library('linux'),
+    meson.get_compiler('vala').find_library('libsodium', dirs: vapi_dir),
+    meson.get_compiler('c').find_library('sodium'),
+]
+
+binman = shared_library('binman', sources,
+    dependencies: dependencies,
+    install: true,
+    vala_gir: 'binman-1.0.gir',
+    install_dir: [true, true, true, true]
+)
+binman_dep = declare_dependency(link_with: binman, include_directories: include_directories('.'))
+
+pkg = import('pkgconfig')
+pkg.generate(binman,
+    version : '0.1',
+    name : 'binman',)
+    
+g_ir_compiler = find_program('g-ir-compiler')
+custom_target('binman typelib', command: [g_ir_compiler, '--shared-library=libbinman.so', '--output', '@OUTPUT@', meson.current_build_dir() / 'binman-1.0.gir'],
+              output: 'binman-1.0.typelib',
+              depends: binman,
+              install: true,
+              install_dir: get_option('libdir') / 'girepository-1.0')

src/meson.build

@@ -0,0 +1,5 @@
+project('Binman', 'vala', 'c')
+vapi_dir = meson.current_source_dir() / 'vapi'
+
+subdir('lib')
+# subdir('cli')

src/vapi/libsodium.vapi

@@ -0,0 +1,237 @@
+/* Vala Bindings for LibSodium
+ * Copyright (c) 2020 Billy Barrow <billyb@pcthingz.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.
+ */
+
+
+ [CCode (cheader_filename = "sodium.h", lower_case_cprefix = "sodium_")]
+ namespace Sodium {
+ 
+   namespace Random {
+     [CCode (cname = "randombytes_SEEDBYTES")]
+     public const size_t SEED_BYTES;
+   
+     [CCode (cname = "randombytes_random")]
+     public uint32 random();
+   
+     [CCode (cname = "randombytes_uniform")]
+     public uint32 random_uniform(uint32 upper_bound);
+   
+     [CCode (cname = "randombytes_buf")]
+     public void random_bytes(uint8[] buffer);
+   
+     [CCode (cname = "randombytes_buf_deterministic")]
+     public void random_bytes_deterministic(uint8[] buffer, uint8[] seed);
+   }
+ 
+   namespace Symmetric {
+     [CCode (cname = "crypto_secretbox_KEYBYTES")]
+     public const size_t KEY_BYTES;
+ 
+     [CCode (cname = "crypto_secretbox_NONCEBYTES")]
+     public const size_t NONCE_BYTES;
+ 
+     [CCode (cname = "crypto_secretbox_MACBYTES")]
+     public const size_t MAC_BYTES;
+ 
+     [CCode (cname = "crypto_secretbox_keygen")]
+     private void key_gen([CCode (array_length = false)]uint8[] key);
+ 
+     public uint8[] generate_key() {
+       uint8[] key = new uint8[KEY_BYTES];
+       key_gen(key);
+       return key;
+     }
+ 
+     [CCode (cname = "crypto_secretbox_easy")]
+     private void secretbox(
+       [CCode (array_length = false)]uint8[] ciphertext,
+       uint8[] message,
+       [CCode (array_length = false)]uint8[] nonce,
+       [CCode (array_length = false)]uint8[] key
+     );
+ 
+     public uint8[] encrypt(uint8[] message, uint8[] key, uint8[] nonce)
+       requires (key.length == KEY_BYTES) 
+       requires (nonce.length == NONCE_BYTES)
+     {
+       // Initialise array for ciphertext
+       size_t ciphertext_size = MAC_BYTES + message.length;
+       uint8[] ciphertext = new uint8[ciphertext_size];
+ 
+       // Encrypt
+       secretbox(ciphertext, message, nonce, key);
+ 
+       // Return ciphertext
+       return ciphertext;
+     }
+ 
+     [CCode (cname = "crypto_secretbox_open_easy")]
+     private int secretbox_open(
+       [CCode (array_length = false)]uint8[] message,
+       uint8[] ciphertext,
+       [CCode (array_length = false)]uint8[] nonce,
+       [CCode (array_length = false)]uint8[] key
+     );
+ 
+     public uint8[]? decrypt(uint8[] ciphertext, uint8[] key, uint8[] nonce)
+       requires (ciphertext.length > MAC_BYTES)
+       requires (key.length == KEY_BYTES) 
+       requires (nonce.length == NONCE_BYTES)
+     {
+       // Initialise array for message
+       size_t message_size = ciphertext.length - MAC_BYTES;
+       uint8[] message = new uint8[message_size];
+ 
+       // Decrypt
+       int status = secretbox_open(message, ciphertext, nonce, key);
+ 
+       // Did it work?
+       if(status != 0) {
+         // No, return null
+         return null;
+       }
+ 
+       return message;
+     }
+   }
+   
+   namespace Asymmetric {
+ 
+     namespace Signing {
+ 
+         [CCode (cname = "crypto_sign_PUBLICKEYBYTES")]
+         public const size_t PUBLIC_KEY_BYTES;
+ 
+         [CCode (cname = "crypto_sign_SECRETKEYBYTES")]
+         public const size_t SECRET_KEY_BYTES;
+ 
+         [CCode (cname = "crypto_sign_BYTES")]
+         public const size_t MAX_HEADER_BYTES;
+ 
+         [CCode (cname = "crypto_sign_keypair")]
+         public void generate_keypair(
+             [CCode (array_length = false)]uint8[] public_key,
+             [CCode (array_length = false)]uint8[] secret_key)
+             requires (public_key.length == PUBLIC_KEY_BYTES)
+             requires (secret_key.length == SECRET_KEY_BYTES);
+             
+         [CCode (cname = "crypto_sign")]
+         private void sign_message(
+             [CCode (array_length = false)] uint8[] signed_message,
+             out int signature_length,
+             uint8[] message,
+             [CCode (array_length = false)] uint8[] secret_key
+         );
+ 
+         public uint8[] sign(
+             uint8[] message,
+             uint8[] secret_key)
+             requires (secret_key.length == SECRET_KEY_BYTES)
+         {
+             int signature_length;
+             uint8[] signed_message = new uint8[MAX_HEADER_BYTES + message.length];
+             sign_message(signed_message, out signature_length, message, secret_key);
+             signed_message.resize(signature_length);
+ 
+             return signed_message;
+         }
+ 
+         [CCode (cname = "crypto_sign_open")]
+         private int sign_open(
+             [CCode (array_length = false)] uint8[] message,
+             out int message_length,
+             uint8[] signed_message,
+             [CCode (array_length = false)] uint8[] public_key
+         );
+ 
+         public uint8[]? verify(
+             uint8[] signed_message,
+             uint8[] public_key)
+             requires (public_key.length == PUBLIC_KEY_BYTES)
+         {
+             int message_length;
+             uint8[] message = new uint8[signed_message.length];
+             if(sign_open(message, out message_length, signed_message, public_key) != 0) {
+                 return null;
+             }
+             message.resize(message_length);
+ 
+             return message;
+         }
+ 
+     }
+ 
+     namespace Sealing {
+ 
+         [CCode (cname = "crypto_box_PUBLICKEYBYTES")]
+         public const size_t PUBLIC_KEY_BYTES;
+ 
+         [CCode (cname = "crypto_box_SECRETKEYBYTES")]
+         public const size_t SECRET_KEY_BYTES;
+ 
+         [CCode (cname = "crypto_box_SEALBYTES")]
+         public const size_t HEADER_BYTES;
+ 
+         [CCode (cname = "crypto_box_keypair")]
+         public void generate_keypair(
+             [CCode (array_length = false)]uint8[] public_key,
+             [CCode (array_length = false)]uint8[] secret_key)
+             requires (public_key.length == PUBLIC_KEY_BYTES)
+             requires (secret_key.length == SECRET_KEY_BYTES);
+ 
+         [CCode (cname = "crypto_box_seal")]
+         private void seal_message(
+             [CCode (array_length = false)] uint8[] ciphertext,
+             uint8[] message,
+             [CCode (array_length = false)] uint8[] public_key
+         );
+ 
+         public uint8[] seal(uint8[] message, uint8[] public_key)
+             requires (public_key.length == PUBLIC_KEY_BYTES)
+         {
+             uint8[] ciphertext = new uint8[HEADER_BYTES + message.length];
+             seal_message(ciphertext, message, public_key);
+             return ciphertext;
+         }
+ 
+         [CCode (cname = "crypto_box_seal_open")]
+         private int seal_open(
+             [CCode (array_length = false)] uint8[] message,
+             uint8[] ciphertext,
+             [CCode (array_length = false)] uint8[] public_key,
+             [CCode (array_length = false)] uint8[] secret_key
+         );
+ 
+         public uint8[]? unseal(
+             uint8[] ciphertext,
+             uint8[] public_key,
+             uint8[] secret_key) 
+             requires (public_key.length == PUBLIC_KEY_BYTES)
+             requires (secret_key.length == SECRET_KEY_BYTES)
+             requires (ciphertext.length > HEADER_BYTES)
+         {
+             uint8[] message = new uint8[ciphertext.length - HEADER_BYTES];
+             if(seal_open(message, ciphertext, public_key, secret_key) != 0){
+                 return null;
+             }
+             return message;
+         }
+         
+     }
+ 
+   }
+   
+ 
+ }