Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
55f8650
WIP: base64/base64url in std.encoding (pure .dag, RFC 4648) + Bytes≅L…
briansrls Jun 23, 2026
f2441b6
base64/base64url in std.encoding (RFC 4648) + Bytes≅List<UInt8> seam
briansrls Jun 23, 2026
da43383
WIP: base64/base64url in std.encoding (pure .dag, RFC 4648) + Bytes≅L…
briansrls Jun 23, 2026
e347afb
base64_decode: fail-closed on invalid input (§5)
briansrls Jun 23, 2026
7244ea1
base64_decode: reject interior '=' and lone trailing sextet (RFC 4648…
briansrls Jun 23, 2026
17f1e75
WIP: base64/base64url in std.encoding (pure .dag, RFC 4648) + Bytes≅L…
briansrls Jun 23, 2026
ceaf5d9
Bytes seam: fail-close the decoy .dag bodies + open-thread marker ((A…
briansrls Jun 23, 2026
8f0ad79
Remove stray probe file zzfc_test.dag (auto-committer captured a thro…
briansrls Jun 23, 2026
7e0472b
Merge remote-tracking branch 'origin/main' into session/keen-wren-182
briansrls Jun 23, 2026
12dc31a
WIP: base64/base64url in std.encoding (pure .dag, RFC 4648) + Bytes≅L…
briansrls Jun 23, 2026
bbf141f
Revert ROADMAP hand-edit: wrong artifact (ROADMAP is a generated proj…
briansrls Jun 23, 2026
fc471dd
Merge remote-tracking branch 'origin/main' into session/keen-wren-182
briansrls Jun 23, 2026
d42bd69
Merge remote-tracking branch 'origin/main' into session/keen-wren-182
briansrls Jun 23, 2026
49df419
std/{bytes,encoding}.dag: remove host-realization / debt marker data …
briansrls Jun 23, 2026
8f6603f
Merge remote-tracking branch 'origin/main' into session/keen-wren-182
briansrls Jun 23, 2026
7a1bf76
std.encoding: ground base64 count carriers as closed sums (§5 constru…
briansrls Jun 23, 2026
3e3073e
Merge remote-tracking branch 'origin/main' into session/keen-wren-182
briansrls Jun 23, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 20 additions & 0 deletions dsl/std/bytes.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
module std.bytes

import std.types { Bytes }
import std.integer { UInt8 }

fn pure_dag_seam_unreachable() -> Int {
1 / 0
}

fn bytes_octets(b: Bytes) -> List<UInt8> {
[pure_dag_seam_unreachable()]
}

fn octets_bytes(o: List<UInt8>) -> Bytes {
o as Bytes
}

fn utf8_encode_bytes(s: String) -> Bytes {
s as Bytes
}
193 changes: 192 additions & 1 deletion dsl/std/encoding.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ module std.encoding

import std.algebra { BoundedLattice }
import std.types { Bytes }
import std.integer { UInt8 }
import std.bytes { pure_dag_seam_unreachable }

type Encoding
= ASCII
Expand Down Expand Up @@ -110,5 +112,194 @@ data encoding_bounded_lattice: BoundedLattice<Encoding> = {
}

fn utf8_decode_bytes(payload: Bytes) -> String {
""
from_code_point(pure_dag_seam_unreachable())
}

type Base64Variant = Standard | UrlSafe

fn base64_alphabet(variant: Base64Variant) -> String {
match variant {
Standard => "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"
UrlSafe => "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_"
}
}

type Base64EncodeBuf
= EncEmpty
| EncOne { b0: Int }
| EncTwo { b0: Int, b1: Int }

type Base64EncodeState {
out: String
buf: Base64EncodeBuf
}

fn base64_octet_int(b: UInt8) -> Int {
b + 0
}

fn base64_sextet_char(alphabet: String, n: Int, divisor: Int) -> String {
char_at(alphabet, (n / divisor) % 64)
}

fn base64_encode_step(st: Base64EncodeState, octet: Int, alphabet: String) -> Base64EncodeState {
match st.buf {
EncEmpty => Base64EncodeState { out: st.out, buf: EncOne { b0: octet } }
EncOne { b0: x } => Base64EncodeState { out: st.out, buf: EncTwo { b0: x, b1: octet } }
EncTwo { b0: x, b1: y } => {
let n = x * 65536 + y * 256 + octet
let quad = concat(
base64_sextet_char(alphabet: alphabet, n: n, divisor: 262144),
base64_sextet_char(alphabet: alphabet, n: n, divisor: 4096),
base64_sextet_char(alphabet: alphabet, n: n, divisor: 64),
char_at(alphabet, n % 64)
)
Base64EncodeState { out: concat(st.out, quad), buf: EncEmpty }
}
}
}

fn base64_encode_flush(st: Base64EncodeState, alphabet: String) -> String {
match st.buf {
EncEmpty => st.out
EncOne { b0: x } => {
let n = x * 65536
concat(
st.out,
base64_sextet_char(alphabet: alphabet, n: n, divisor: 262144),
base64_sextet_char(alphabet: alphabet, n: n, divisor: 4096),
"=="
)
}
EncTwo { b0: x, b1: y } => {
let n = x * 65536 + y * 256
concat(
st.out,
base64_sextet_char(alphabet: alphabet, n: n, divisor: 262144),
base64_sextet_char(alphabet: alphabet, n: n, divisor: 4096),
base64_sextet_char(alphabet: alphabet, n: n, divisor: 64),
"="
)
}
}
}

fn base64_encode(octets: List<UInt8>, variant: Base64Variant) -> String {
let alphabet = base64_alphabet(variant: variant)
let st = fold(octets,
init: Base64EncodeState { out: "", buf: EncEmpty },
f: (acc, octet) => base64_encode_step(st: acc, octet: base64_octet_int(b: octet), alphabet: alphabet)
)
base64_encode_flush(st: st, alphabet: alphabet)
}

fn base64_char_value(c: String, variant: Base64Variant) -> Int? {
let cp = code_point(c)
if cp >= 65 && cp <= 90 {
Present { value: cp - 65 }
} else if cp >= 97 && cp <= 122 {
Present { value: cp - 71 }
} else if cp >= 48 && cp <= 57 {
Present { value: cp + 4 }
} else {
match variant {
Standard =>
if cp == 43 { Present { value: 62 } }
else if cp == 47 { Present { value: 63 } }
else { none }
UrlSafe =>
if cp == 45 { Present { value: 62 } }
else if cp == 95 { Present { value: 63 } }
else { none }
}
}
}

fn base64_collect_values(s: String, i: Int, len: Int, variant: Base64Variant, seen_pad: Bool, acc: List<Int>) -> List<Int>? {
if i >= len {
Present { value: acc }
} else {
let c = char_at(s, i)
if c == "=" {
base64_collect_values(s: s, i: i + 1, len: len, variant: variant, seen_pad: true, acc: acc)
} else if seen_pad {
none
} else {
match base64_char_value(c: c, variant: variant) {
Absent => none
Present { value: v } =>
base64_collect_values(s: s, i: i + 1, len: len, variant: variant, seen_pad: false, acc: acc |> list_push(v))
}
}
}
}

type Base64DecodeBuf
= DecEmpty
| DecOne { v0: Int }
| DecTwo { v0: Int, v1: Int }
| DecThree { v0: Int, v1: Int, v2: Int }

type Base64DecodeState {
out: List<Int>
buf: Base64DecodeBuf
}

fn base64_decode_step(st: Base64DecodeState, v: Int) -> Base64DecodeState {
match st.buf {
DecEmpty => Base64DecodeState { out: st.out, buf: DecOne { v0: v } }
DecOne { v0: a } => Base64DecodeState { out: st.out, buf: DecTwo { v0: a, v1: v } }
DecTwo { v0: a, v1: b } => Base64DecodeState { out: st.out, buf: DecThree { v0: a, v1: b, v2: v } }
DecThree { v0: a, v1: b, v2: c } => {
let n = a * 262144 + b * 4096 + c * 64 + v
let byte0 = (n / 65536) % 256
let byte1 = (n / 256) % 256
let byte2 = n % 256
Base64DecodeState {
out: st.out |> list_push(byte0) |> list_push(byte1) |> list_push(byte2),
buf: DecEmpty
}
}
}
}

fn base64_decode_flush(st: Base64DecodeState) -> List<Int>? {
match st.buf {
DecEmpty => Present { value: st.out }
DecOne { v0: _ } => none
DecTwo { v0: a, v1: b } => {
let n = a * 262144 + b * 4096
Present { value: st.out |> list_push((n / 65536) % 256) }
}
DecThree { v0: a, v1: b, v2: c } => {
let n = a * 262144 + b * 4096 + c * 64
Present { value: st.out |> list_push((n / 65536) % 256) |> list_push((n / 256) % 256) }
}
}
}

fn base64_octet_of_int(n: Int) -> UInt8 {
n
}

fn base64_decode_values(vals: List<Int>) -> List<UInt8>? {
let st = fold(vals,
init: Base64DecodeState { out: [], buf: DecEmpty },
f: (acc, v) => base64_decode_step(st: acc, v: v)
)
match base64_decode_flush(st: st) {
Absent => none
Present { value: octets } => Present { value: octets |> map(n => base64_octet_of_int(n: n)) }
}
}

fn base64_decode(s: String, variant: Base64Variant) -> List<UInt8>? {
match base64_collect_values(s: s, i: 0, len: string_length(s), variant: variant, seen_pad: false, acc: []) {
Absent => none
Present { value: vals } =>
match base64_decode_values(vals: vals) {
Absent => none
Present { value: octets } => Present { value: octets }
}
}
}
87 changes: 87 additions & 0 deletions dsl/test/claim/base64_rfc4648_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,87 @@
module test.claim.base64_rfc4648_witness

import std.logic { Bool }
import std.integer { UInt8 }
import std.bytes { bytes_octets, octets_bytes, utf8_encode_bytes }
import std.encoding { Base64Variant, Standard, UrlSafe, base64_encode, base64_decode, utf8_decode_bytes }

fn b64_std_of_utf8(s: String) -> String {
base64_encode(octets: bytes_octets(b: utf8_encode_bytes(s: s)), variant: Standard)
}

data url_witness_octets: List<UInt8> = [251, 255, 191]

test fn bytes_octets_iso_holds() -> Bool {
let b = utf8_encode_bytes(s: "foobar")
octets_bytes(o: bytes_octets(b: b)) == b
}

test fn utf8_total_direction_holds() -> Bool {
utf8_decode_bytes(payload: utf8_encode_bytes(s: "naïve")) == "naïve"
}

test fn base64_octet_roundtrip_holds() -> Bool {
let o = bytes_octets(b: utf8_encode_bytes(s: "foobar"))
match base64_decode(s: base64_encode(octets: o, variant: Standard), variant: Standard) {
Present { value: d } => d == o
Absent => false
}
}

test fn base64_decode_rejects_invalid_char_holds() -> Bool {
match base64_decode(s: "Zm9*", variant: Standard) {
Present { value: _ } => false
Absent => true
}
}

test fn base64_decode_rejects_cross_variant_char_holds() -> Bool {
match base64_decode(s: "Zm9-", variant: Standard) {
Present { value: _ } => false
Absent => true
}
}

test fn base64_decode_rejects_interior_pad_holds() -> Bool {
match base64_decode(s: "Zg==Zg==", variant: Standard) {
Present { value: _ } => false
Absent => true
}
}

test fn base64_decode_rejects_lone_sextet_holds() -> Bool {
match base64_decode(s: "Zm9vY", variant: Standard) {
Present { value: _ } => false
Absent => true
}
}

test fn base64_decode_accepts_unpadded_holds() -> Bool {
let o = bytes_octets(b: utf8_encode_bytes(s: "foob"))
match base64_decode(s: "Zm9vYg", variant: Standard) {
Present { value: d } => d == o
Absent => false
}
}

test fn base64_rfc4648_golden_vectors_holds() -> Bool {
b64_std_of_utf8(s: "") == ""
&& b64_std_of_utf8(s: "f") == "Zg=="
&& b64_std_of_utf8(s: "fo") == "Zm8="
&& b64_std_of_utf8(s: "foo") == "Zm9v"
&& b64_std_of_utf8(s: "foob") == "Zm9vYg=="
&& b64_std_of_utf8(s: "fooba") == "Zm9vYmE="
&& b64_std_of_utf8(s: "foobar") == "Zm9vYmFy"
}

test fn base64url_alphabet_golden_holds() -> Bool {
base64_encode(octets: url_witness_octets, variant: Standard) == "+/+/"
&& base64_encode(octets: url_witness_octets, variant: UrlSafe) == "-_-_"
}

test fn base64url_roundtrip_holds() -> Bool {
match base64_decode(s: base64_encode(octets: url_witness_octets, variant: UrlSafe), variant: UrlSafe) {
Present { value: d } => d == url_witness_octets
Absent => false
}
}
36 changes: 36 additions & 0 deletions src/v1/stage0/src/v1_interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4433,6 +4433,42 @@ fn eval_builtin(
Ok(Some(Value::Str(text)))
}

"bytes_octets" => {
let bytes = expect_byte_vec(positional.first().copied(), "bytes_octets")?;
let items: Vec<Value> = bytes.iter().map(|b| Value::Int(*b as i64)).collect();
Ok(Some(list_value(items)))
}

"octets_bytes" => {
let arg = positional.first().copied().ok_or_else(|| InterpError::TypeError {
msg: "octets_bytes requires a List<UInt8> argument".to_string(),
})?;
let items = free_monoid_to_vec(arg).ok_or_else(|| InterpError::TypeError {
msg: "octets_bytes expects a List<UInt8>".to_string(),
})?;
let mut out: Vec<Value> = Vec::with_capacity(items.len());
for item in &items {
match item {
Value::Int(n) if (0..=255).contains(n) => out.push(Value::Int(*n)),
other => {
return Err(InterpError::TypeError {
msg: format!(
"octets_bytes expects octets 0..255, got element {}",
other.type_label()
),
})
}
}
}
Ok(Some(list_value(out)))
}

"utf8_encode_bytes" => {
let s = expect_str(positional.first().copied(), "utf8_encode_bytes")?;
let items: Vec<Value> = s.as_bytes().iter().map(|b| Value::Int(*b as i64)).collect();
Ok(Some(list_value(items)))
}

"discriminant" => match positional.first() {
Some(Value::Variant { variant_name, .. }) => {
Ok(Some(Value::Str(resolve_sym(*variant_name))))
Expand Down