Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
d334847
NUMERIC-BIT-0: model the fixed-width word and bit-operation substrate…
Sep 18, 2026
a5cddd2
NUMERIC-BIT-0: split the bitwise claim into discriminators; parenthes…
Sep 18, 2026
fed5a40
NUMERIC-BIT-0: fix the mistranscribed bitwise operand and claim the t…
Sep 18, 2026
d778dcb
NUMERIC-BIT-0: derive the modulus once per width; carry the consumer …
Sep 19, 2026
5eead3d
NUMERIC-BIT-0: fix the closed-set recomputation class, not only the c…
Sep 19, 2026
9befdd7
NUMERIC-BIT-0: bind the frontier rows against bound_dissolution's rea…
Sep 19, 2026
b290752
NUMERIC-BIT-0: enrol the consumer frontier in the census that compute…
Sep 19, 2026
fa465ac
NUMERIC-BIT-0: refuse an unrealizable width before accumulating octets
Sep 19, 2026
a40faa2
NUMERIC-BIT-0: unbind the frontier triggers that cited a module absen…
Sep 19, 2026
94f7248
NUMERIC-BIT-0: qualify operand premises, refuse a negative octet coun…
Sep 19, 2026
fdcdff5
Merge remote-tracking branch 'origin/main' into session/sharp-raven-413
Sep 19, 2026
faa8903
Merge main and admit utf8_decode_octets' members through the checked …
Sep 19, 2026
4ccc8bd
NUMERIC-BIT-0: qualify the octet projection; delete the orphaned word…
Sep 19, 2026
8d81d86
NUMERIC-BIT-0: make the qualification a carrier, not a check every he…
Sep 19, 2026
7a0fea5
Thread base64_encode refusal at approval_device_wire path_segment
Sep 19, 2026
97888f6
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 19, 2026
356ed1c
Export the qualified-octet unwrap; revert the plans-doc edit that for…
Sep 19, 2026
069c7b2
Merge remote-tracking branch 'origin/session/sharp-raven-413' into se…
Sep 19, 2026
c705aec
Restore the plans-doc repoint; CI auto-heal regenerated its projection
Sep 19, 2026
d2e1d9c
Make the typecheck green control assert acceptance, and cite BigEndia…
Sep 19, 2026
92e2d4d
Retire the second stale onboarding citation, and pin refusal CAUSES n…
Sep 19, 2026
b8abbf7
Unescape the record-literal braces in the typecheck probe sources
Sep 19, 2026
2aebbdd
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 19, 2026
a13e29f
Withdraw the unexecutable typecheck witness and declare the wall unwi…
Sep 19, 2026
e10d852
Merge remote-tracking branch 'origin/main' into session/sharp-raven-413
Sep 19, 2026
223a2ba
WIP ENCODING-0 cut 2: octet span, CBOR, DER, X.509, App Attest parse …
Sep 19, 2026
c5bed74
ENCODING-0 cut 2: witnesses green (CBOR 18, DER 17, App Attest 19); a…
Sep 19, 2026
f10406a
Bound content reads to their span: an empty BIT STRING or KeyUsage no…
Sep 19, 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
552 changes: 548 additions & 4 deletions dag/extdeps/apple/app_attest.dag

Large diffs are not rendered by default.

20 changes: 17 additions & 3 deletions dag/extdeps/cloud/gcp/secret_manager.dag
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module extdeps.cloud.gcp.secret_manager

import std.encoding { Standard, base64_decode, base64_encode, utf8_decode_bytes }
import std.bytes { bytes_octets, octets_bytes, utf8_encode_bytes }
import std.bytes { bytes_octets, octets_bytes, utf8_encode_bytes, pure_dag_seam_unreachable_string }
import extdeps.cloud.gcp.iam { GcpBinding, GcpPolicy }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
Expand Down Expand Up @@ -199,11 +199,25 @@ fn sm_resolved_version_identity_is_well_formed(name: String) -> Bool {
}
}

// base64_encode gained a refusal channel when NUMERIC-BIT-0 (gunbc#11627) routed its packing
// through std.machine_word: it refuses an octet outside the byte range, where it previously
// multiplied one into a plausible wrong string. THE ARM IS UNREACHABLE HERE, and that is a
// statement about this call and not about base64_encode: the octets are the UTF-8 encoding of a
// String, so every member is a byte by construction and no in-range input can reach the refusal.
// An unreachable arm still has to answer, and "" is a valid base64 encoding -- of the empty
// credential -- so returning it would conflate a refusal with a real answer at a secret-provisioning
// boundary. std.bytes' divergent seam is the corpus's declared idiom for an arm that cannot be
// reached; it diverges rather than fabricating, which is the loud half of DESIGN section 5.
// This function's signature is deliberately unchanged: threading an Optional to the two actuators
// that call it would put a refusal channel where no refusal can arise.
fn encode_sm_access_version_payload_wire(credential: Secret) -> String {
base64_encode(
match base64_encode(
octets: bytes_octets(b: utf8_encode_bytes(s: credential as String)),
variant: Standard
)
) {
Present { value: wire } => wire
Absent => pure_dag_seam_unreachable_string()
}
}

fn decode_sm_access_version_payload_wire(data_b64: String) -> SmAccessVersionPayloadDecodeOutcome {
Expand Down
315 changes: 315 additions & 0 deletions dag/extdeps/ietf/cbor.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,315 @@
module extdeps.ietf.cbor

import std.integer { UInt8 }
import std.octet_span {
OctetSpan, OctetReadRefusal, OctetInputTruncated, OctetUnsignedTooWide, OctetWordRefused,
OctetUnsignedRead, OctetUnsignedReady, OctetUnsignedRefused,
OctetSpanRead, OctetSpanReady, OctetSpanRefused,
octet_at, octet_bit_field, octet_read_unsigned_be, octet_span_read, octet_span_equals, octet_span_is,
}
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }

// CBOR, RFC 8949 (Concise Binary Object Representation), as a total decoder over one octet input.
//
// Only what a named consumer decodes is modeled: App Attest attestation and assertion objects, their
// COSE credential keys and authenticator-data extensions (extdeps.apple.app_attest). Every data item
// is decoded structurally; strings are carried as spans into the input rather than copied, so a
// consumer compares or re-reads the exact wire octets.
//
// The accepted form is RFC 8949 section 4.2.1's deterministic encoding, and every departure from it
// is its own refusal rather than a best-effort reading, because a protocol that verifies bytes must
// not accept two encodings of one value:
// * an argument not in its shortest form -> CborNoncanonicalArgument
// * an indefinite-length string, array or map -> CborIndefiniteLengthUnsupported
// * additional information 28-30 (reserved, 3.1) -> CborReservedAdditionalInfo
// * a map with two equal keys (5.6) -> CborDuplicateMapKey
// * octets left over after the top-level item -> CborTrailingInput
// Floats and simple values other than false/true/null have no consumer and refuse as unsupported.
// An 8-octet argument refuses as too wide: std.machine_word does not yet realize 64-bit words, and
// no consumed App Attest field needs one.
data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "www.rfc-editor.org/rfc/rfc8949"
}
}

type CborEntry {
key: CborItem
key_encoding: OctetSpan
value: CborItem
}

type CborItem
= CborUnsigned { value: Int }
| CborNegative { argument: Int }
| CborBytes { span: OctetSpan }
| CborText { span: OctetSpan }
| CborArray { items: List<CborItem> }
| CborMap { entries: List<CborEntry> }
| CborTagged { tag: Int, item: CborItem }
| CborFalse
| CborTrue
| CborNull

type CborRefusal
= CborTruncated { at: Int, needed: Int, available: Int }
| CborReservedAdditionalInfo { at: Int, info: Int }
| CborIndefiniteLengthUnsupported { at: Int }
| CborNoncanonicalArgument { at: Int }
| CborArgumentTooWide { at: Int }
| CborSimpleValueUnsupported { at: Int, info: Int }
| CborDuplicateMapKey { at: Int }
| CborTrailingInput { at: Int, remaining: Int }
| CborNestingExhausted { at: Int }

// One decoded item and the offset just past it.
type CborStep
= CborStepped { item: CborItem, end: Int }
| CborStepRefused { cause: CborRefusal }

type CborDecode
= CborDecoded { item: CborItem }
| CborRefused { cause: CborRefusal }

// Nesting bound. Every item consumes at least one octet, so the recursion also descends on the
// input; the depth bound makes the refusal for pathological nesting a named arm, not a stack.
data cbor_max_depth: Int = 16

type CborHead {
major: Int
argument: Int
end: Int
}

type CborHeadRead
= CborHeadReady { head: CborHead }
| CborHeadIndefinite { major: Int }
| CborHeadSimple { info: Int, end: Int }
| CborHeadRefused { cause: CborRefusal }

fn cbor_refusal_of_octet_read(cause: OctetReadRefusal) -> CborRefusal {
match cause {
OctetInputTruncated { at: a, needed: n, available: v } => CborTruncated { at: a, needed: n, available: v }
OctetUnsignedTooWide { at: a, octets: _ } => CborArgumentTooWide { at: a }
OctetWordRefused { at: a } => CborArgumentTooWide { at: a }
}
}

// The smallest argument each extended form may carry (RFC 8949 4.2.1 preferred serialization).
fn cbor_extended_minimum(octets: Int) -> Int {
if octets == 1 { 24 } else if octets == 2 { 256 } else { 65536 }
}

fn cbor_extended_octets(info: Int) -> Int {
if info == 24 { 1 } else if info == 25 { 2 } else if info == 26 { 4 } else { 8 }
}

// The initial byte and its argument: major type = the top 3 bits, additional information = the low
// 5, both read through std.octet_span's machine-word bit field.
fn cbor_read_head(input: List<UInt8>, at: Int) -> CborHeadRead {
match octet_at(input: input, at: at) {
Absent => CborHeadRefused { cause: CborTruncated { at: at, needed: 1, available: 0 } }
Present { value: initial } =>
match octet_bit_field(octet: initial, shift: 5, mask: 7) {
Absent => CborHeadRefused { cause: CborArgumentTooWide { at: at } }
Present { value: major } =>
match octet_bit_field(octet: initial, shift: 0, mask: 31) {
Absent => CborHeadRefused { cause: CborArgumentTooWide { at: at } }
Present { value: info } => cbor_read_argument(input: input, at: at, major: major, info: info)
}
}
}
}

fn cbor_read_argument(input: List<UInt8>, at: Int, major: Int, info: Int) -> CborHeadRead {
if info >= 28 && info <= 30 {
CborHeadRefused { cause: CborReservedAdditionalInfo { at: at, info: info } }
} else if major == 7 && info >= 20 && info != 24 && info != 31 {
CborHeadSimple { info: info, end: at + 1 }
} else if info < 24 {
CborHeadReady { head: CborHead { major: major, argument: info, end: at + 1 } }
} else if info == 31 {
CborHeadIndefinite { major: major }
} else {
let octets = cbor_extended_octets(info: info)
match octet_read_unsigned_be(input: input, at: at + 1, octets: octets) {
OctetUnsignedRefused { cause: c } => CborHeadRefused { cause: cbor_refusal_of_octet_read(cause: c) }
OctetUnsignedReady { value: v, end: e } =>
if v < cbor_extended_minimum(octets: octets) {
CborHeadRefused { cause: CborNoncanonicalArgument { at: at } }
} else if major == 7 {
CborHeadRefused { cause: CborSimpleValueUnsupported { at: at, info: info } }
} else {
CborHeadReady { head: CborHead { major: major, argument: v, end: e } }
}
}
}
}

fn cbor_simple_item(at: Int, info: Int, end: Int) -> CborStep {
if info == 20 {
CborStepped { item: CborFalse, end: end }
} else if info == 21 {
CborStepped { item: CborTrue, end: end }
} else if info == 22 {
CborStepped { item: CborNull, end: end }
} else {
CborStepRefused { cause: CborSimpleValueUnsupported { at: at, info: info } }
}
}

fn cbor_decode_item(input: List<UInt8>, at: Int, depth: Int) -> CborStep {
if depth <= 0 {
CborStepRefused { cause: CborNestingExhausted { at: at } }
} else {
match cbor_read_head(input: input, at: at) {
CborHeadRefused { cause: c } => CborStepRefused { cause: c }
CborHeadIndefinite { major: _ } => CborStepRefused { cause: CborIndefiniteLengthUnsupported { at: at } }
CborHeadSimple { info: info, end: end } => cbor_simple_item(at: at, info: info, end: end)
CborHeadReady { head: head } => cbor_decode_body(input: input, at: at, head: head, depth: depth)
}
}
}

fn cbor_string_span(input: List<UInt8>, head: CborHead) -> OctetSpanRead {
octet_span_read(input: input, at: head.end, length: head.argument)
}

fn cbor_decode_body(input: List<UInt8>, at: Int, head: CborHead, depth: Int) -> CborStep {
if head.major == 0 {
CborStepped { item: CborUnsigned { value: head.argument }, end: head.end }
} else if head.major == 1 {
CborStepped { item: CborNegative { argument: head.argument }, end: head.end }
} else if head.major == 2 || head.major == 3 {
match cbor_string_span(input: input, head: head) {
OctetSpanRefused { cause: c } => CborStepRefused { cause: cbor_refusal_of_octet_read(cause: c) }
OctetSpanReady { span: span } =>
if head.major == 2 {
CborStepped { item: CborBytes { span: span }, end: span.end }
} else {
CborStepped { item: CborText { span: span }, end: span.end }
}
}
} else if head.major == 4 {
cbor_decode_array(input: input, at: head.end, remaining: head.argument, depth: depth, acc: [])
} else if head.major == 5 {
cbor_decode_map(input: input, at: head.end, remaining: head.argument, depth: depth, acc: [])
} else {
match cbor_decode_item(input: input, at: head.end, depth: depth - 1) {
CborStepRefused { cause: c } => CborStepRefused { cause: c }
CborStepped { item: inner, end: end } => CborStepped { item: CborTagged { tag: head.argument, item: inner }, end: end }
}
}
}

// A count larger than the octets left cannot be satisfied (each item takes at least one octet), so
// it refuses as truncation before any element is read.
fn cbor_count_fits(input: List<UInt8>, at: Int, remaining: Int) -> Bool {
remaining <= count(input) - at
}

fn cbor_decode_array(input: List<UInt8>, at: Int, remaining: Int, depth: Int, acc: List<CborItem>) -> CborStep {
if remaining == 0 {
CborStepped { item: CborArray { items: acc }, end: at }
} else if !cbor_count_fits(input: input, at: at, remaining: remaining) {
CborStepRefused { cause: CborTruncated { at: at, needed: remaining, available: count(input) - at } }
} else {
match cbor_decode_item(input: input, at: at, depth: depth - 1) {
CborStepRefused { cause: c } => CborStepRefused { cause: c }
CborStepped { item: item, end: end } =>
cbor_decode_array(input: input, at: end, remaining: remaining - 1, depth: depth, acc: acc |> list_push(item))
}
}
}

fn cbor_key_seen(input: List<UInt8>, entries: List<CborEntry>, key: OctetSpan) -> Bool {
any(entries, e => octet_span_equals(input: input, a: e.key_encoding, b: key))
}

fn cbor_decode_map(input: List<UInt8>, at: Int, remaining: Int, depth: Int, acc: List<CborEntry>) -> CborStep {
if remaining == 0 {
CborStepped { item: CborMap { entries: acc }, end: at }
} else if !cbor_count_fits(input: input, at: at, remaining: remaining * 2) {
CborStepRefused { cause: CborTruncated { at: at, needed: remaining * 2, available: count(input) - at } }
} else {
match cbor_decode_item(input: input, at: at, depth: depth - 1) {
CborStepRefused { cause: c } => CborStepRefused { cause: c }
CborStepped { item: key, end: key_end } => {
let key_span = OctetSpan { start: at, end: key_end }
if cbor_key_seen(input: input, entries: acc, key: key_span) {
CborStepRefused { cause: CborDuplicateMapKey { at: at } }
} else {
match cbor_decode_item(input: input, at: key_end, depth: depth - 1) {
CborStepRefused { cause: c } => CborStepRefused { cause: c }
CborStepped { item: value, end: value_end } =>
cbor_decode_map(
input: input, at: value_end, remaining: remaining - 1, depth: depth,
acc: acc |> list_push(CborEntry { key: key, key_encoding: key_span, value: value })
)
}
}
}
}
}
}

// One item starting at `at` that must end exactly at `end`: used for an embedded CBOR value whose
// extent the enclosing structure already fixed.
fn cbor_decode_exact(input: List<UInt8>, at: Int, end: Int) -> CborDecode {
match cbor_decode_item(input: input, at: at, depth: cbor_max_depth) {
CborStepRefused { cause: c } => CborRefused { cause: c }
CborStepped { item: item, end: e } =>
if e == end {
CborDecoded { item: item }
} else if e < end {
CborRefused { cause: CborTrailingInput { at: e, remaining: end - e } }
} else {
CborRefused { cause: CborTruncated { at: end, needed: e - end, available: 0 } }
}
}
}

// A whole input that is exactly one CBOR data item.
fn cbor_decode(input: List<UInt8>) -> CborDecode {
cbor_decode_exact(input: input, at: 0, end: count(input))
}

// ── Reading decoded maps ─────────────────────────────────────────────────────────────────────
// Protocol maps are keyed by text strings (App Attest) or small integers (COSE). A key is looked up
// by its WIRE octets, so a consumer states the exact encoding it expects and nothing is transcoded.

fn cbor_text_key_is(input: List<UInt8>, key: CborItem, expected: List<UInt8>) -> Bool {
match key {
CborText { span: span } => octet_span_is(input: input, span: span, expected: expected)
_ => false
}
}

fn cbor_map_text_value(input: List<UInt8>, entries: List<CborEntry>, key: List<UInt8>) -> CborItem? {
fold(entries, init: none, f: (acc, e) =>
if cbor_text_key_is(input: input, key: e.key, expected: key) { Present { value: e.value } } else { acc })
}

// A COSE integer label: non-negative n is CborUnsigned n; negative -1 - a is CborNegative a.
fn cbor_int_key_is(key: CborItem, label: Int) -> Bool {
match key {
CborUnsigned { value: v } => label >= 0 && v == label
CborNegative { argument: a } => label < 0 && (0 - 1 - a) == label
_ => false
}
}

fn cbor_map_int_value(entries: List<CborEntry>, label: Int) -> CborItem? {
fold(entries, init: none, f: (acc, e) =>
if cbor_int_key_is(key: e.key, label: label) { Present { value: e.value } } else { acc })
}

fn cbor_int_value(item: CborItem) -> Int? {
match item {
CborUnsigned { value: v } => Present { value: v }
CborNegative { argument: a } => Present { value: 0 - 1 - a }
_ => none
}
}
Loading