Jadpo is experimental and not ready for production. These docs follow the compiler's main branch as of 30 Oct 2026. What's built · Install 0.1.0
jadpo
Reference: Standard library

Standard library

Encodings

On this page

The encoding operations turn bytes into text and back: Base64 and Base64url for bytes sent as text, hexadecimal for digests, UTF-8 for text as bytes, and percent-encoding for a part of a link. Each is called as encoding.<name>.

Operation Gives Fails SQL form
to_base64(bytes) Text, standard alphabet, padded translate(encode(x, 'base64'), E'\n', '')
from_base64(text) Bytes malformed none
to_base64url(bytes) Text, URL alphabet, unpadded, as Identity's signed parts are rtrim(translate(encode(x, 'base64'), E'+/\n', '-_'), '=')
from_base64url(text) Bytes; padding refused malformed none
to_hex(bytes) Text, lowercase encode(x, 'hex')
from_hex(text) Bytes; either case malformed none
to_utf8(text) Bytes convert_to(x, 'UTF8')
from_utf8(bytes) Text; invalid UTF-8 refused, never replaced malformed none
to_url_component(text) Text with everything but RFC 3986's unreserved characters percent-encoded as UTF-8 none

Writing never fails. Reading fails malformed for text that isn't the encoding at all, and reads only the one form writing gives.

A bakery's photos, attachments and links go through hash.sha256 and each encoding. hash.sha256 takes any value built on Bytes, such as PhotoBytes, or on Text, whose UTF-8 it hashes (hash.sha256(email)). A digest is Bytes, which encoding writes as text:

example
type PhotoBytes = Bytes {    max_length: 5000000}type PhotoKey = Text {}type ShareCode = Text {}type SentAttachment = Text {    max_length: 7000000}type RecipeTitle = Text {    max_length: 100}type LinkPart = Text {}type AttachmentUnreadable = Failure {    kind: FailureKind.invalid_value}type AttachmentTooLarge = Failure {    kind: FailureKind.invalid_value}/// A photo's content key: the same bytes always give the same 64/// lowercase hexadecimal digits.function photo_key(photo: PhotoBytes) -> PhotoKey {    return PhotoKey(encoding.to_hex(hash.sha256(photo)))}/// A short code for a recipe, from its title's UTF-8, safe in a URL.function share_code(title: RecipeTitle) -> ShareCode {    return ShareCode(encoding.to_base64url(hash.sha256(title)))}/// An attachment a client sends as Base64 text, as its bytes.function attachment(    sent: SentAttachment) fails AttachmentUnreadable, AttachmentTooLarge -> PhotoBytes {    var sent_bytes: Bytes = attempt encoding.from_base64(sent) {        malformed: AttachmentUnreadable    }    return attempt PhotoBytes(sent_bytes) {        max_length: AttachmentTooLarge    }}/// A photo sent back as Base64 text.function sent_photo(photo: PhotoBytes) -> LinkPart {    return LinkPart(encoding.to_base64(photo))}/// A photo's key read back as its 32 bytes, in either case.function key_bytes(key: PhotoKey) fails AttachmentUnreadable, AttachmentTooLarge -> PhotoBytes {    var sent_bytes: Bytes = attempt encoding.from_hex(key) {        malformed: AttachmentUnreadable    }    return attempt PhotoBytes(sent_bytes) {        max_length: AttachmentTooLarge    }}/// A share code read back as the digest it was written from.function code_digest(code: ShareCode) fails AttachmentUnreadable, AttachmentTooLarge -> PhotoBytes {    var sent_bytes: Bytes = attempt encoding.from_base64url(code) {        malformed: AttachmentUnreadable    }    return attempt PhotoBytes(sent_bytes) {        max_length: AttachmentTooLarge    }}/// A title through its UTF-8 bytes and back; bytes that aren't UTF-8 are/// refused, never replaced.function title_again(title: RecipeTitle) fails AttachmentUnreadable -> LinkPart {    var title_back: Text = attempt encoding.from_utf8(encoding.to_utf8(title)) {        malformed: AttachmentUnreadable    }    return LinkPart(title_back)}/// A title as it goes in a link a sign-in email carries.function link_part(title: RecipeTitle) -> LinkPart {    return LinkPart(encoding.to_url_component(title))}

The values in the test are published ones: SHA-256 of "abc" is NIST's FIPS 180-4 example, and the Base64 of "f", "fo" and "foo" are RFC 4648's test vectors:

example
test "hashing and the encodings give what the page says" {    var abc_photo: PhotoBytes = attempt attachment("YWJj")    assert photo_key(        abc_photo    ) == "ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad"    assert sent_photo(abc_photo) == "YWJj"    var f: PhotoBytes = attempt attachment("Zg==")    assert sent_photo(f) == "Zg=="    var fo: PhotoBytes = attempt attachment("Zm8=")    assert sent_photo(fo) == "Zm8="    assert attachment("Zg") fails AttachmentUnreadable    assert attachment("Zm9v YmFy") fails AttachmentUnreadable    var key: PhotoBytes = attempt key_bytes(        "BA7816BF8F01CFEA414140DE5DAE2223B00361A396177A9CB410FF61F20015AD"    )    assert sent_photo(key) == "ungWv48Bz+pBQUDeXa4iI7ADYaOWF3qctBD/YfIAFa0="    assert key_bytes("ba78z6") fails AttachmentUnreadable    assert share_code("Rye loaf") == "_Hbznn1YqQK2jbbPF34hJmf_7AY2WLJKH4ZE68W-z_I"    var code_bytes: PhotoBytes = attempt code_digest("_Hbznn1YqQK2jbbPF34hJmf_7AY2WLJKH4ZE68W-z_I")    assert sent_photo(code_bytes) == "/Hbznn1YqQK2jbbPF34hJmf/7AY2WLJKH4ZE68W+z/I="    assert code_digest("_Hbznn1YqQK2jbbPF34hJmf_7AY2WLJKH4ZE68W-z_I=") fails AttachmentUnreadable    var title_back: LinkPart = attempt title_again("Crème brûlée")    assert title_back == "Crème brûlée"    assert link_part("Crème brûlée & rye") == "Cr%C3%A8me%20br%C3%BBl%C3%A9e%20%26%20rye"}

malformed

malformed is the only condition a decoder fails on. No decoder can be proved while compiling, so malformed is settled only by an attempt, never by an option or a proof.

One text for each value

What decodes reads only what encodes writes, so no two texts read as the same bytes:

  • from_base64 takes standard, padded Base64 only, its length a multiple of four, and from_base64url takes unpadded Base64url only. Both refuse white space, the other alphabet's characters and bits after the last byte that aren't zero (RFC 4648, 3.5).
  • A Bytes value on the wire is read and written by the same function, so a request, a response and json.read read bytes alike: a request whose Base64 isn't padded breaks format.
  • from_hex takes an even number of digits in either case. to_hex writes lowercase, and to_url_component's escapes are uppercase (RFC 3986, 2.1).

There is no from_url_component: the runtime decodes paths and query strings before your code sees them (Paths and placeholders). to_url_component is for a link your code builds, such as an email's sign-in link.

No base32 and no compression

There is no base32 operation and no compression. gzip is read only inside the file readers, with max_unpacked_size: (Data formats).

Related

Markdown for agents: /docs/encodings.md.Built from Jadpo main at a707efb.