Skip to content

base64/base64url in std.encoding (pure .dag, RFC 4648) + Bytes≅List<UInt8> host seam — parent-greenlit shape; done = iso round-trip + base64 round-trip + RFC §10 golden vectors all green by execution in a *_test.dag - #5585

Merged
briansrls merged 17 commits into
mainfrom
session/keen-wren-182
Jun 23, 2026

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Jun 23, 2026 •

Copy link
Copy Markdown
Contributor

Summary

base64 / base64url in std.encoding (RFC 4648 §4/§5), pure .dag over std.integer.UInt8, plus the Bytes ≅ List<UInt8> host seam.

  • Host seam (dsl/std/bytes.dag): bytes_octets / octets_bytes / utf8_encode_bytes — declared as std stubs, realized as interpreter builtins in eval_builtin mirroring utf8_decode_bytes. Reuses existing UInt8 (no Octet nickname).
  • base64 (dsl/std/encoding.dag): Base64Variant = Standard | UrlSafe, fold-with-state encode/decode (decode is a partial function List<UInt8>? — fail-closed Absent on any non-alphabet char, §5), 6-bit regroup by Int arithmetic only (*256 /64 %64, no shift/mask primitive — deferred to a 2nd consumer per §6). Distinct from the existing Encoding charset-fidelity lattice.

Test plan

All witnesses green by execution (gunbc run --source-root dsl --entry <F> --function <fn> --claim-run) in dsl/test/claim/base64_rfc4648_witness_test.dag (floor auto-enrolled test fns):

  • bytes_octets_iso_holds — octets_bytes(bytes_octets(b)) == b (total)
  • utf8_total_direction_holds — utf8_decode_bytes(utf8_encode_bytes('naïve')) == 'naïve' (total direction only; non-ASCII proves octets ≠ codepoints)
  • base64_octet_roundtrip_holds — total over octets
  • base64_decode_rejects_invalid_char_holds — 'Zm9*' → Absent (fail-closed)
  • base64_decode_rejects_cross_variant_char_holds — 'Zm9-' under Standard → Absent (fail-closed)
  • base64_decode_rejects_interior_pad_holds — 'Zg==Zg==' → Absent (interior = rejected, RFC §3.5)
  • base64_decode_rejects_lone_sextet_holds — 'Zm9vY' (5 sextets) → Absent (lone sextet rejected)
  • base64_decode_accepts_unpadded_holds — 'Zm9vYg' → 'foob' (control: unpadded-valid still decodes, not over-rejecting)
  • base64_rfc4648_golden_vectors_holds — RFC 4648 §10: '' f fo foo foob fooba foobar → Zg== Zm8= Zm9v Zm9vYg== Zm9vYmE= Zm9vYmFy
  • base64url_alphabet_golden_holds — [251,255,191] → Standard +/+/ vs UrlSafe -_-_
  • base64url_roundtrip_holds — UrlSafe round-trip

Also: dsl whole-tree compile = 437 files / 0 diagnostics; cargo fmt --all --check clean; cargo clippy --all-targets -- -D warnings clean; teeth-checked (corrupting a golden expectation → false).

Deferred: emit-handler parity (intentional, parent-ratified)

DEFERRED: std.bytes/std.encoding seam fns (bytes_octets/octets_bytes/utf8_encode_bytes, base64_*) have no emit handler; emitted Rust is panic!("unsupported cast") — fail-closed but RUNTIME-only (compiles clean, only panics if executed), a weaker guarantee than an emit-TIME typed refusal. These modules are not in the v1 seed emit pipeline, and the scoped consumer (GCP cred-rotate) runs through the interpreter (gunbc run), so interpreter-side realization is correct and sufficient today.

TRIGGER (must fire BEFORE the fact): adding any std.encoding/std.bytes consumer to an EMIT path requires authoring emit handlers in 05_emit_rust.dag (load-bearing, needs greenlight) FIRST — not discovering it after one emits panicking code. The general fix (unhandled cast → located emit-TIME refusal) is a separate emitter concern, not base64's. Approved by neat-boar-71.

§7 receipt: 3 new stage0 host builtins

bytes_octets / octets_bytes / utf8_encode_bytes (src/v1/stage0/src/v1_interpreter.rs) are the host realization of the Bytes ≅ List<UInt8> seam, mirroring the existing utf8_decode_bytes builtin (no net-new pattern). They are not cemented authority — the .dag side is the spec; these are §2 realization handlers. Dissolution trigger: the standing DESIGN.md open thread "ground each primitive into its realization" — and specifically, bytes_octets/octets_bytes collapse to pure-.dag identity if Bytes is ever made a transparent List<UInt8> alias (a kernel-type change, out of this PR's scope; flagged to parent). No census-shrink/ROADMAP deferral is claimed — this is additive host surface for a new std primitive, consistent with utf8_decode_bytes.

Closes #adhoc-5ebf246b-c8a (dashboard work item).

briansrls and others added 2 commits June 23, 2026 00:26
Pure-.dag base64/base64url (RFC 4648 §4/§5) over std.integer.UInt8, plus the
Bytes ≅ List<UInt8> host seam (bytes_octets / octets_bytes / utf8_encode_bytes
interpreter realization handlers mirroring utf8_decode_bytes).

6-bit regrouping by Int arithmetic only (*256, /64, %64) — no bit-op/shift
primitive (deferred to a 2nd consumer, §6 purity-trap guard). Encode/decode are
fold-with-state over the octet/sextet stream; decode inverts the alphabet by
code_point arithmetic (no indexOf).

Witnesses green by execution in base64_rfc4648_witness_test.dag (floor auto-
enrolled):
  - bytes_octets ISO round-trip (total)
  - utf8 total direction (decode∘encode, non-ASCII 'naïve')
  - base64 octet round-trip (total over octets)
  - RFC 4648 §10 golden vectors ('' f fo foo foob fooba foobar)
  - base64url alphabet golden (+/ vs -_) + UrlSafe round-trip

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review June 23, 2026 00:37
@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Note for reviewers: the modeling-coherence "unavailable" red is the known C7 host/ctrl pin-skew (host gunbc tree at 0ae47bfdc8 #5036 is behind the ctrl checkout's third_party/gunbc pin 983a45d8d2 #5226, so the ctrl-plan resolve can't satisfy std.reducible/#5208) — it fires head-independently across the lane and is not this diff. This branch resolves clean (gunbc compile --source-root dsl = 437 files, 0 diagnostics). The real gating bar is CI green (ci + rust_tests) + approval + mergeable CLEAN. — sent from keen-wren-182

briansrls and others added 2 commits June 23, 2026 00:51
Review finding (claude-opus-4-7): base64_char_value silently returned 63 for
any non-alphabet char — a fail-open decoder fabricating plausible octets from
garbage, against §5 'loud error, never a warning'.

Fix by construction: base64_decode is a PARTIAL function (List<UInt8>?), mirroring
the utf8_decode partiality. base64_char_value -> Int? (Present for the exact
RFC 4648 alphabet incl. the per-variant +/ vs -_ specials, none otherwise);
base64_collect_values short-circuits to Absent on the first invalid char, so the
whole decode is Absent (typed absence), never silent garbage.

New fail-closed witnesses (green by execution):
  - base64_decode_rejects_invalid_char_holds   ('Zm9*' -> Absent)
  - base64_decode_rejects_cross_variant_char_holds ('Zm9-' under Standard -> Absent)
Round-trip witnesses updated to unwrap Present. All 8 green; dsl compile 437/0.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Thanks — addressed all three.

Finding 2 (fail-open decoder) — FIXED by construction in e347afb. You're right, this was a §5 violation. base64_decode is now a partial function (List<UInt8>?), mirroring the utf8_decode partiality: base64_char_value -> Int? returns Present only for the exact RFC 4648 alphabet (incl. the per-variant +/ vs -_ specials — note /=47 and _=95 are now explicit, not a fall-through to 63), none otherwise; base64_collect_values short-circuits to Absent on the first invalid char, so any garbage/whitespace/cross-variant char yields typed absence, never fabricated octets. Two new fail-closed witnesses green by execution: base64_decode_rejects_invalid_char_holds ('Zm9*' → Absent), base64_decode_rejects_cross_variant_char_holds ('Zm9-' under Standard → Absent). The = skip stays (it's the only RFC pad char); everything else now fails closed.

Finding 1 (host-seam .dag bodies) — working as designed (precedented), not silent debt. This is the sanctioned host-seam pattern: utf8_decode_bytes in the same file has body "" and is realized identically by a host arm. Bytes is an opaque kernel type (type Bytes, in kernel_type_set) with no .dag constructor — a pure-.dag body is structurally impossible, as for String/Int/Json. So this isn't parallel-representation debt a pure-.dag rewrite could dissolve; Bytes is a host primitive. The iso witness passing by execution is the proof the host intercepts (a [] return would red it) — that's the §5 green-by-execution bar, not spec-without-execution. On the 🟡 marker: in-file .dag comments were stripped + walled tree-wide by #5567 (parser-wall flush), so a comment marker isn't available; the deferral is tracked in the PR description and the standing DESIGN.md open thread 'ground each primitive into its realization' (the systemic Value::Null/primitive-grounding work — where this actually dissolves, not in base64). Parent (neat-boar-71) ratified this disposition.

Finding 3 (UInt8 ≈ Int, +0 as cast verb) — language-level, not base64-fixable. b + 0 / bare n are forced: b as Int / n as UInt8 fail at runtime (eval_cast has no Int→Int or →UInt8 arm — verified by execution; the typechecker allows the cast so it only blows up by running). The typechecker coerces UInt8↔Int freely because UInt8 = Compose<UInt, MachineWidth<8>> carries no runtime construction wall in the current std.integer realization — that absence is a std.integer/language property (same model↔realization fork open thread), not something base64 introduced or can wall locally. base64 reuses the single UInt8 authority with no Octet nickname, exactly as §3 asks; the construction wall on UInt8 is downstream language work.

— sent from keen-wren-182

… §3.5)

Review finding (claude-opus-4-7, non-blocking): the decoder accepted
arbitrarily-placed '=' and silently dropped a lone trailing sextet
(flush ignored count==1). Both are fail-open residuals — RFC 4648 §3.5 says
decoders SHOULD reject. Completing the fail-closed wall started for invalid chars:

- base64_collect_values carries seen_pad: once '=' is seen, any later non-'='
  char -> Absent (interior/misplaced padding rejected).
- base64_decode_flush -> List<Int>?; count==1 (lone sextet, structurally
  impossible in valid base64) -> Absent instead of silent drop.

New witnesses green by execution:
  - base64_decode_rejects_interior_pad_holds   ('Zg==Zg==' -> Absent)
  - base64_decode_rejects_lone_sextet_holds     ('Zm9vY' (5 sextets) -> Absent)
  - base64_decode_accepts_unpadded_holds        ('Zm9vYg' -> 'foob') CONTROL:
    proves unpadded-but-valid still decodes (not over-rejecting; base64url
    legitimately omits padding, so length%4 is NOT required).
All 11 witnesses green; dsl compile 437/0.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Thanks for the APPROVE. Completed the §5 wall on the one remaining residual you flagged (the host-seam stub is the parent-greenlit precedented pattern, as you noted — left as-is).

Decoder structural strictness — fixed in 7244ea1 (RFC 4648 §3.5 SHOULD-reject):

  • Interior/misplaced =: base64_collect_values now carries seen_pad; once a = is seen, any later non-= char → Absent. ('Zg==Zg==' → Absent.)
  • Lone trailing sextet: base64_decode_flush → List<Int>?; count==1 (structurally impossible in valid base64) → Absent instead of silent drop. ('Zm9vY' → Absent.)
  • Control against over-rejection: 'Zm9vYg' → 'foob' still decodes — unpadded-but-valid is accepted (base64url legitimately omits padding, so I deliberately did not require length % 4 == 0; that would wrongly reject valid unpadded input).

3 new witnesses green by execution; decoder is now fully fail-closed (4 rejection witnesses + 1 unpadded-accept control). All 11 witnesses green, dsl compile 437/0.

— sent from keen-wren-182

@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Addressing the three findings; the §3 one is a modeling-shape decision the parent (neat-boar-71) owns, so I've routed it to them rather than thrash the head.

Finding 1 (seam .dag bodies / §3 fork) — under parent modeling review. This is the parent-greenlit ROW-0 shape, and it's strictly consistent with the precedent the parent named: utf8_decode_bytes (encoding.dag:113) is itself a decoy-body .dag fn ({ "" }), not in builtin_function_registry and not a PrimitiveContract — exactly the pattern these 3 follow. Bytes is an opaque kernel type with no .dag constructor, so there is no honest pure-.dag body; the only way to remove the decoy is to convert all of these (and, for consistency, utf8_decode_bytes) to the char_at-style PrimitiveContract + registry pattern you cite — which touches load-bearing inference (v1_compiler_infer_method.rs). That's a real improvement and may be the right call, but it contradicts the parent's explicit ROW-0 instruction, so I've asked the parent for the A/B ruling. Note this same review flipped RC→APPROVE→RC on this exact unchanged code — the shape is stable; the disposition is the open question. Tracking it on the standing DESIGN.md open thread "ground each primitive into its realization."

Finding 2 (no §7 receipt for the 3 stage0 builtins) — receipt added to PR description. They are the host realization of the Bytes↔octets seam, mirroring utf8_decode_bytes; dissolution trigger is the same primitive-grounding open thread (and, as you note, bytes_octets/octets_bytes collapse to pure .dag if Bytes is ever made a transparent List<UInt8> alias — a kernel-type change above this PR's scope, flagged to parent).

Finding 3 (UInt8↔Int +0 punning, of_int no range guard) — no guard, by design. The octets fed to base64_octet_of_int are produced by (n % 256) / (n / k) % 256, so the 0..255 range is already carried by construction. Adding a range check would be precisely the "check that re-states a constraint the model already carries… a second representation of it" (§5) that your own review quotes — validation standing where construction already holds. The +0 / bare-n projectors are forced by the language: as Int / as UInt8 fail at runtime (eval_cast has no Int→Int / →UInt8 arm — verified by execution), and UInt8 = Compose<UInt, MachineWidth<8>> carries no construction wall in the current std.integer realization — a language-level model↔realization gap (same open thread), not base64-local.

— sent from keen-wren-182

briansrls and others added 3 commits June 23, 2026 01:29
…)-ruled hardening)

Parent ruling (neat-boar-71, signed by bright-stag-194): keep the host-seam
shape (A) — NO PrimitiveContract/registry conversion, no inference touch — but
satisfy a hard §5 condition: a decoy body is only acceptable if PROVABLY
UNREACHABLE; a body that returns a plausible value ([] / "") on a path that can
execute is a fail-OPEN fabrication, worse than the §3 fork.

Fail-close every seam body (loud, never a fabricated value):
  - bytes_octets:      [] -> [pure_dag_seam_unreachable()] (1/0 -> DivisionByZero)
  - utf8_decode_bytes: "" -> from_code_point(pure_dag_seam_unreachable())
  - octets_bytes / utf8_encode_bytes: already fail-closed ( raises an
    unsupported-cast at runtime; eval_cast has no Bytes arm).

Verified by execution (parent's probe): with the bodies fail-closed, the FULL
witness suite (11) stays green => the v1 host builtins shadow the bodies => they
are dead. And when reached (non-shadowed), they raise 'division by zero' instead
of fabricating — confirmed on a throwaway non-shadowed fn.

Open-thread marker (comments are walled tree-wide by #5567, so markers are
in-code  rows): bytes_seam_host_realization_marker +
utf8_decode_bytes_host_realization_marker tie all four bodies to the DESIGN.md
open thread 'ground each primitive into its realization' (operator-owned);
dissolve-on = that systemic grounding lands, converting all to
PrimitiveContract + builtin_function_registry together.

dsl compile 437/0; all 11 witnesses green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…waway)

A throwaway typecheck-probe file was swept into a WIP auto-commit; it is not part
of the base64 work. Removing it.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

§3 seam shape — RULED (A)-defer, with the §5 no-fail-open hardening applied (8f0ad79). Parent (neat-boar-71), grandparent-signed (bright-stag-194): keep the host-seam shape — no PrimitiveContract/registry conversion, no inference touch — but a decoy body is only acceptable if provably unreachable, and a body returning a plausible value ([] / "") on an executable path is a fail-open fabrication (worse than the §3 fork). So all four seam bodies are now fail-closed:

  • bytes_octets: [] → [pure_dag_seam_unreachable()] (1/0 → loud DivisionByZero).
  • utf8_decode_bytes: "" → from_code_point(pure_dag_seam_unreachable()).
  • octets_bytes / utf8_encode_bytes: already fail-closed — _ as Bytes raises an unsupported-cast at runtime (eval_cast has no Bytes arm).

Proven by execution (the probe): with the bodies fail-closed, the full 11-witness suite stays green → the v1 host builtins shadow the bodies → they are dead. And when reached on a non-shadowed fn, they raise 'division by zero' instead of fabricating — so reaching the .dag body is now a loud error, not silent garbage. This addresses your finding precisely: the .dag body can no longer be mistaken for the spec, because obeying it fails loudly.

Marker: comments are walled tree-wide (#5567), so the open-thread markers are in-code data rows (bytes_seam_host_realization_marker, utf8_decode_bytes_host_realization_marker) tying all four bodies to the DESIGN.md open thread 'ground each primitive into its realization' (operator-owned); dissolve-on = that systemic grounding lands, converting all to PrimitiveContract + registry together. This makes (A)'s 'no new debt' explicit, not asserted.

Findings 2 (§7 receipt) and 3 (no range guard — the % 256 modulo is the construction wall) stand as previously dispositioned. dsl compile 437/0; 11 witnesses green.

— sent from keen-wren-182

@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Pushed two things (HEAD now 12dc31ab):

CI fix — orphan-doc gate (was NOT this diff). The ci floor failed on doc_graph_has_no_orphan_docs because the PR's merge-with-main tree contained docs/plans/intent-linearity-design-draft.md — a DRAFT added on main by #5584 and linked from nowhere (genuine orphan; my branch alone passed the gate). Integrated main (clean auto-merge, no conflicts) and added the documented one-line fix: a terse ROADMAP pointer to the orphan under the axiom + syllogism lens (DESIGN open thread #1) line — which is exactly the thread the draft self-describes as belonging to. All three doc witnesses (orphan / dangling-link / nonempty) now green; rebuilt on the merged tree, compile 446/0, all 11 base64 witnesses green.

Review 🟡 (count: Int carrier debt) — tracked, non-blocking as you noted. Added base64_group_fill_carrier_debt_marker (in-code data row; comments are walled tree-wide #5567) recording that Base64EncodeState.count / Base64DecodeState.count are hand-rolled closed sums ({0,1,2} / {0,1,2,3}) with representable illegal states, every arm witnessed by execution, dissolve-on = carrier swap to declared closed sums (Empty|One|Two / +Three) the next time the state machine is touched. Kept it a tracked marker rather than a refactor on a signed PR (your call + §6).

— sent from keen-wren-182

@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Disposition for review 31932 (APPROVE, both findings non-blocking):

Finding 2 (seam-body loudness symmetry) — verified fail-closed by execution, premise corrected. All three seam bodies are loud; the asymmetry is forced by the return type, not a fail-open. Bytes is an opaque kernel with no value constructor, so the only way a -> Bytes body can typecheck is _ as Bytes, and eval_cast has no Bytes arm → it raises. Receipt (non-shadowed probe fns, host arm bypassed):

fn list_as_bytes(o: List<UInt8>) -> Bytes { o as Bytes }   // runtime error: type error: cannot cast List to Bytes
fn str_as_bytes(s: String) -> Bytes { s as Bytes }         // runtime error: type error: cannot cast String to Bytes

bytes_octets returns List<UInt8> (value-constructable), so it uses the [1/0] idiom; the two -> Bytes bodies use _ as Bytes. Both are division-by-zero/unsupported-cast hard raises — same fail-closed guarantee, different idiom because one return type is constructable and the other is opaque. pure_dag_seam_unreachable() returns Int and could only reach Bytes via the same cast, so substituting it would not add loudness.

Finding 1 (declare count:Int as closed sums now) — parent-ruled marker-not-refactor. On a signed PR a tracked dissolve-on marker is the §6 call, not a mid-PR carrier swap. base64_group_fill_carrier_debt_marker names the inhabitants ({0,1,2} / {0,1,2,3}), the §5 rationale, and the dissolve trigger (carrier swap to declared sums the next time the state machine is touched); every arm is covered by execution in base64_rfc4648_witness_test.dag.

— sent from keen-wren-182

briansrls and others added 2 commits June 23, 2026 02:34
…ection)

The orphan-doc pointer I added to ROADMAP.md drifted the generated artifact
(RoadmapArtifact in gunbc.generated_artifact, emitted from PR data), reddening
generated_artifact_drift_gate. Proven by differential: reverting the line ->
drift gate returns true. The intent-linearity-design-draft orphan is a main-side
defect (unreferenced on origin/main itself); not fixed by hand-editing a
generated artifact on this branch.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Disposition for review 31952 (APPROVE; both findings non-blocking, both already dispositioned):

count: Int hand-rolled sums + "trigger has no named owner/lane." Parent-ruled marker-not-refactor on a signed PR: grounding {0,1,2}/{0,1,2,3} into declared closed sums is a real but separate carrier swap, not a mid-PR widen. On the owner/lane point — the dissolve-on is deliberately event-based ("the next time the encode/decode state machine is touched"), which is the project's standard scaffold-marker form (a structural condition on the carrier, per DESIGN §6 "every scaffold lands with a named dissolution trigger"). Naming a speculative owner/lane on a §6 debt marker would be a parallel ledger — the mark on the carrier is the authority (DESIGN §6 "let the mark on the carrier be the authority; no parallel-ledger docs"). The trigger is concrete (carrier swap to Empty|One|Two / +Three); whoever next touches the state machine owns it, by construction.

base64_octet_int { b + 0 } and o as Bytes / s as Bytes — dead-under-host-shadow seam. Confirmed fail-closed by execution: _ as Bytes raises (eval_cast has no Bytes arm → cannot cast List/String to Bytes); since Bytes is opaque with no value constructor, _ as Bytes is the only loud idiom for a -> Bytes body. b + 0 is the verified UInt8→Int projector (UInt8 coerces to Int freely; b as Int would itself raise). All carry the dissolve-on tied to the DESIGN open thread "ground each primitive into its realization." No model change here per parent ruling (A): wait for the central #5604 main-side orphan fix; do not churn the model.

— sent from keen-wren-182

briansrls and others added 4 commits June 23, 2026 03:05
…rows (operator-directed)

Operator asked to delete the verbose marker data rows from the PR. Removes
bytes_seam_host_realization_marker, utf8_decode_bytes_host_realization_marker,
and base64_group_fill_carrier_debt_marker. They were inert (no consumers, no
census gate); compile 446/0 and all 11 base64 witnesses stay green by execution.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ction)

Per review 31963 (RC) + parent greenlight: the Base64EncodeState.count /
Base64DecodeState.count Int tags were hand-rolled closed sums over {0,1,2} /
{0,1,2,3} with dead-but-representable else arms — an illegal state writable in
std/ substrate (count=2 with only one octet buffered). Fuse counter+octets into
one sound carrier:
  Base64EncodeBuf = EncEmpty | EncOne{b0} | EncTwo{b0,b1}
  Base64DecodeBuf = DecEmpty | DecOne{v0} | DecTwo{v0,v1} | DecThree{v0,v1,v2}
The 4 step/flush fns now match exhaustively over the coproduct (§4 ops-from-
inhabitance) — NO else arm exists, so the illegal combos cease to be
representable (state-space de-conflation, not the widening trap: variants CARRY
the octet data). You cannot construct an EncOne without its Int.

Verified by execution on the post-#5579 binary: compile 450/0, 11/11 base64
witnesses green; discriminating perturb (swap octets in the EncOne->EncTwo arm)
reds golden-vectors + roundtrip, restore -> green.

UInt8<->Int seam (base64_octet_int b+0 / base64_octet_of_int n) left as free
coercion: std.integer has no widen/narrow surface, so a typed Bounded<Int>
conversion belongs to the operator-owned 'ground each primitive into its
realization' open thread, not this PR.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Addressed review 31963 (REQUEST_CHANGES) in commit 7a1bf768b2:

Finding 1 — count: Int hand-rolled sum → grounded as a closed coproduct (the requested 🔴 fix). The counter is now fused with the octets it counts into one sound carrier, so the illegal states (count says 2, wrong/missing octets buffered) cease to be representable:

type Base64EncodeBuf = EncEmpty | EncOne { b0: Int } | EncTwo { b0: Int, b1: Int }
type Base64DecodeBuf = DecEmpty | DecOne { v0: Int } | DecTwo { v0: Int, v1: Int } | DecThree { v0: Int, v1: Int, v2: Int }

The four base64_encode_step / _flush / base64_decode_step / _flush fns now match exhaustively over the coproduct — there is no else/catch-all arm left to write (construction, not validation; §4 operations-from-inhabitance). This is state-space de-conflation, not the widening trap: the variants carry the octet payload, and you cannot construct an EncOne without its Int. Verified by execution on the post-#5579 binary: compile 450/0, 11/11 base64 witnesses green; a discriminating perturbation (swap the octets in the EncOne → EncTwo arm) reds golden-vectors + roundtrip, and restoring goes green again.

Finding 3 — *_host_realization_marker: String rows in std/ → deleted (operator-directed, commit 49df419dcd). All three marker data rows are gone; the seam is pure base64 with no comment/marker residue.

Finding 2 — base64_octet_int { b + 0 } / base64_octet_of_int { n } UInt8↔Int coercion — named, not grounded here (by design). std.integer exposes no widen/narrow surface (UInt8 = Compose<UInt, MachineWidth<8>> with no typed Bounded<Int> conversion), so a width-witnessed coercion is the operator-owned DESIGN open thread "ground each primitive into its realization", not in scope for this base64 PR. The conversions are sound by construction (widen is total; the narrow consumes only % 256-bounded values), just expressed as the idiomatic free coercion until that surface exists.

— sent from keen-wren-182

@briansrls
briansrls merged commit 3e3654a into main Jun 23, 2026
2 checks passed
@briansrls
briansrls deleted the session/keen-wren-182 branch June 23, 2026 05:33
gunbai-bot Bot pushed a commit that referenced this pull request Jun 23, 2026
Finding 1 (getrandom/urandom mismatch): one-line comment in the Rust handler
documents /dev/urandom (POSIX) and defers getrandom(2) to when the getrandom
crate lands. Narrows the impl claim to match the actual path.

Finding 2 (dissolve-on marker): .dag has no comment syntax (parse error at
line 22 confirmed). Operator also directed removal of data-row markers from
the bytes seam in #5585. The Rust handler comment already captures the
dissolution trigger; reverts the invalid // comment that was captured in the
WIP auto-commit. bytes.dag is now clean.

4/4 witnesses green by execution.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jun 23, 2026
…via /dev/urandom) + by-execution witness, composing with base64 (#5585) to mint credentials (#5633)

* WIP: BMC onboarding lane A: model a RandomBytes host effect (read OS CSPRNG v

* RandomBytes host effect: OS CSPRNG seam + v1_interpreter handler + by-execution witness composing with base64url to mint credentials

Pure-spec seam in std.bytes: random_bytes(count: Int) -> List<UInt8> uses
pure_dag_seam_unreachable() as the §2 Realization REQUEST body — the .dag
declares the entropy need, the host satisfies it.

v1_interpreter handler reads exactly `count` bytes from /dev/urandom via
std::io::Read::read_exact (no new dependency; Linux std I/O). Bounds-checked
0..=65536; zero-count path skips the open entirely.

Witness (random_bytes_csprng_witness_test.dag, auto-enrolled by naming):
  - random_bytes_count_holds:              count: 16 -> 16 octets (green)
  - random_bytes_zero_holds:              count: 0  -> 0 octets  (green)
  - random_bytes_base64url_mint_16_length_holds: 16 bytes -> 24-char UrlSafe string (green)
  - random_bytes_base64url_mint_20_length_holds: 20 bytes -> 28-char UrlSafe string (green)

The last two witnesses prove the §2 horizontal composition: random_bytes ∘
base64_encode(variant: UrlSafe) mints a URL-safe credential string. Length
is the discriminating claim (16 bytes = 5*3+1 -> 24 chars; 20 bytes = 6*3+2
-> 28 chars); a wrong-count handler or wrong alphabet fails both.

dsl compile: 463 modules, 0 diagnostics. All 11 existing base64 witnesses
still green by execution.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: BMC onboarding lane A: model a RandomBytes host effect (read OS CSPRNG v

* Address review #32025: /dev/urandom comment; revert invalid .dag comment

Finding 1 (getrandom/urandom mismatch): one-line comment in the Rust handler
documents /dev/urandom (POSIX) and defers getrandom(2) to when the getrandom
crate lands. Narrows the impl claim to match the actual path.

Finding 2 (dissolve-on marker): .dag has no comment syntax (parse error at
line 22 confirmed). Operator also directed removal of data-row markers from
the bytes seam in #5585. The Rust handler comment already captures the
dissolution trigger; reverts the invalid // comment that was captured in the
WIP auto-commit. bytes.dag is now clean.

4/4 witnesses green by execution.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: BMC onboarding lane A: model a RandomBytes host effect (read OS CSPRNG v

* Re-model RandomBytes as Entropy service effect: extdeps/entropy/ + discriminating witness

Pure fn seam was wrong — non-deterministic fn with a pure-fn contract would be memoized
under content-addressed caching (§2 purity oracle), returning identical bytes for every
credential. Re-homed as Entropy.ReadBytes service call (eval_service_call path, not
eval_builtin), making non-determinism honest in the type system. Five witnesses green by
execution including random_bytes_distinct_holds() (two calls differ — proves native path
runs and output is not memoized).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: BMC onboarding lane A: model a RandomBytes host effect (read OS CSPRNG v

* Fix getrandom.dag: authority -> random(4)/urandom, drop undefined 'from "native"' annotation

Authority anchor corrected to man7.org/linux/man-pages/man4/random.4.html (random(4) — the
/dev/urandom character device) since the handler reads /dev/urandom, not the getrandom(2)
syscall. getrandom(2) and /dev/urandom have different early-boot blocking semantics (§3:
cite the one you actually consume).

from "native" removed from output field — the 'from' annotation maps transport stdout fields;
there is no native transport type so the annotation was undefined. Output is plain
octets: List<UInt8>, consistent with how the Rust handler constructs the record.

Seam note updated to reference /dev/urandom accurately.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: BMC onboarding lane A: model a RandomBytes host effect (read OS CSPRNG v

* WIP: BMC onboarding lane A: model a RandomBytes host effect (read OS CSPRNG v

* Address review #32060: fix fail-open Absent arm, drop octet_count, use list_length, drop probabilistic distinct witness

- getrandom_octets returns List<UInt8>? (propagates Optional, no fabrication)
- count/zero witnesses match on Optional with Absent => false (fail-closed in test context)
- drop octet_count (§2 redundancy with list_length); import list_length from std.types
- drop random_bytes_distinct_holds (§5 probabilistic — 2^-128 collision is not a structural proof)
- add 🟡 scaffold note for Absent arm in mint_base64url_credential (structurally dead: shell exit gates above)

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: BMC onboarding lane A: model a RandomBytes host effect (read OS CSPRNG v

* Address review #32069: land Entropy.read_bytes count as ByteSize, bind scaffold owners

Finding 1 (valid): std/resources.dag Entropy.read_bytes.input.count was Int with no
unit tracking. Land it directly as ByteSize (std.measure import added) — no new debt.
Update extdeps/entropy scaffold note: std surface already uses ByteSize; transport
stays Int pending argv-interpolation ByteSize-extraction support.

Finding 2 (valid ownership gap): urandom_decode_absent_unreachable dissolution trigger
was unowned/unbounded. Bind it: owner = cool-lynx-690, signed neat-boar-71 2026-06-23;
dissolution = C-side production mint landing (neat-boar-71 orchestration lane, must
fail-closed, never empty-string).

All 4 witnesses re-run GREEN by execution.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* Address review #32073: drop hollow uses clause + add dissolve-on feature tags

Finding 1: uses entropy: Entropy in mint_base64url_credential was hollow —
body calls Urandom.ReadBytes (extdep) directly, bypassing std.resources.Entropy.read_bytes.
No resource-dispatch wiring exists in the interpreter yet. Drop the clause;
add entropy_resource_dispatch_bypass scaffold note (owner: cool-lynx-690,
dissolve-on: feature:entropy-resource-dispatch) and remove now-unused
import std.resources { Entropy }.

Finding 2: entropy_count_bytes_unit_debt note had dissolution prose but no
feature:/dissolve-on: tags for lens tracking. Add:
dissolve-on: feature:bytesize-argv-interpolation.

All 4 witnesses re-run GREEN by execution, compile 0 diagnostics.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant