Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
778d914
The kernel was installable all along, and the export profile it unblo…
Sep 5, 2026
3a30d1d
Model the slicer, and refuse it: the ABI floor is measured, not inferred
Sep 5, 2026
d630df4
The denominator was caller-supplied, and one witness was proving it
Sep 5, 2026
4687b82
A seal decides who may mint, never that the value handed in was earned
Sep 5, 2026
947464c
The process authority already existed; I re-derived it and wrote pros…
Sep 5, 2026
bedf243
The receipt was real and its subject was still substitutable
Sep 5, 2026
fe7f7b7
Substitution was closed; KIND was not, and `true` exits zero on every…
Sep 5, 2026
c250431
The passing arm was public, the budget was a copied number, and I del…
Sep 5, 2026
7fb8efa
The criterion was caller-selected, and verified bytes decayed into a …
Sep 5, 2026
7cc6952
Merge remote-tracking branch 'origin/main' into session/crisp-ibex-71…
Sep 5, 2026
eda09b4
The completeness law already existed, and my repair copied the local …
Sep 5, 2026
46fc82b
The roster can be the malformed one, and the measurements had no cons…
Sep 5, 2026
25a0eff
Merge remote-tracking branch 'origin/main' into session/crisp-ibex-71…
Sep 5, 2026
c731549
Model the printer file channel, and refuse to spell a credential into…
Sep 5, 2026
44409d4
Adjudicate the netrc_content declarer move on the wave-admission roster
Sep 5, 2026
5b2df2f
wip: local transport changes before merging main
Sep 6, 2026
db1dfb7
Merge main: adopt the printer endpoint authority that already exists …
Sep 6, 2026
cfc5779
Consume main's printer endpoint authority; close the exfiltration, ra…
Sep 6, 2026
786ca10
Narrow delivery to local execution and admit exactly one canonical en…
Sep 6, 2026
7c6fe3b
Drop the payload realization on every exit path; retire the stale adm…
Sep 6, 2026
ee5cd66
Observe the container instead of asking a roster whether it wrote one
Sep 6, 2026
97eb672
Make the locus roster unavoidable, and stop a 404 from erasing a receipt
Sep 6, 2026
e4abb0c
Narrow what a record may say, so impossible transitions stop being sp…
Sep 6, 2026
a88411a
A receipt cannot pin a version its own resource does not name
Sep 6, 2026
fc37ab1
Merge main
Sep 6, 2026
205fd77
A brand is a name, not a constructor; and "one adapter" had three rea…
Sep 6, 2026
bb44084
Bind the mint names explicitly, and stop two comments asserting what …
Sep 6, 2026
8cdad79
A successful delivery must not exit non-zero
Sep 6, 2026
f2c817d
Consume the Port that exists, bind Network explicitly, unsay "nothing…
Sep 6, 2026
1462d55
Drop the import B8 made stale, because an unused edge resolves bare n…
Sep 6, 2026
525a621
Name the residue on the refused arm too, so a leaked credential canno…
Sep 6, 2026
b0af5b6
Refuse a receipt that names two secrets, and name the residue on ever…
Sep 6, 2026
71aa00b
Cover the materialization failures too: a partial netrc and an abando…
Sep 6, 2026
951eb37
Stop rendering a credential locator, require the seal at the real bou…
Sep 6, 2026
2db905e
Make the contradictory endpoint unspellable, retire the abandoned-rep…
Sep 6, 2026
05e8f4d
Merge remote-tracking branch 'origin/main' into session/crisp-ibex-71…
Sep 6, 2026
faa003b
Correct four claims the code contradicts, including two the branch ha…
Sep 6, 2026
86eb11c
Keep credential residue out of the payload's classifier, move the pee…
Sep 6, 2026
b33cea7
Test the join, not the value below it: the residue pair proved nothin…
Sep 6, 2026
558e882
The refusal survived an attempt to falsify it, so the receipt now say…
Sep 6, 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
74 changes: 73 additions & 1 deletion dag/extdeps/cloud/gcp/secret_manager.dag
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ import v2.std.optional { Present }
// coverage, not a binding. Named explicitly so this module carries its own edges.
import extdeps.cloud.gcp.gcp { GcpProjectId }
import extdeps.cloud.gcp.errors { GcpErrorShape }
import extdeps.transports.rest { RestOutcome }
import v2.std.operation_argv { OperationRef }

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
Expand Down Expand Up @@ -204,6 +205,62 @@ fn decode_sm_access_version_payload_wire(data_b64: String) -> SmAccessVersionPay
}
}

// THE VERSION ID IS READ OUT OF THE RESOLVED IDENTITY, NEVER CARRIED BESIDE IT.
//
// A resolved identity is "projects/P/secrets/S/versions/V", and V is the only place the version
// lives. Taking the resource and the version as two independent values is what lets a caller state a
// resource ending /versions/7 next to a version of 12 -- a receipt that disagrees with itself.
//
// AN EARLIER REVISION OF THIS FUNCTION CLAIMED TO BE TOTAL BY CONSTRUCTION, AND A WITNESS IN ANOTHER
// MODULE FALSIFIED IT. The claim was that SmResolvedVersionIdentity can only be minted by
// decode_sm_resolved_version_identity_wire, so the split below could not fail and its fallback was
// unreachable. But the brand is `NonEmptyStr where brand(...)`, and a brand is a NAME, not a
// constructor: any module can write `"anything" as SmResolvedVersionIdentity` and one already did.
// The decoder is A minter, never THE minter. So the old fallback -- returning the whole string as
// the version id -- was reachable, and it answered "not-a-version-resource" to the question "which
// version is this", which is the fabricated plausible output §5 forbids outright.
//
// SO IT REFUSES INSTEAD OF PROJECTING. The validation the brand does not perform happens here, at
// the point of use, and a malformed identity yields a typed refusal rather than a plausible-looking
// segment. This is validation and not construction, and it is honest about being so: the rung climbs
// when the decoder owns a carrier no other module can spell, at which point this refusal arm becomes
// unreachable FOR REAL and can be deleted with the evidence to say why.
type SmVersionIdProjection
= SmVersionIdProjected { version: NonEmptyStr }
| SmVersionIdNotAVersionResource { supplied: String }

fn sm_resolved_version_id(identity: SmResolvedVersionIdentity) -> SmVersionIdProjection {
let text = identity as String
if !sm_resolved_version_identity_is_well_formed(name: text) {
SmVersionIdNotAVersionResource { supplied: text }
} else {
match split(s: text, delimiter: "/versions/") |> skip(n: 1) |> first {
Present { value: version_id } => SmVersionIdProjected { version: version_id as NonEmptyStr }
Absent => SmVersionIdNotAVersionResource { supplied: text }
}
}
}

// THE SECRET HALF OF THE RESOLVED RESOURCE, projected for the same reason the version half is: a
// caller that needs to know WHICH secret the service actually versioned cannot get it by trusting
// what it asked for. Only projecting the version invited a receipt whose identity came half from
// the request and half from the response, which is a contradiction no consumer can detect.
type SmVersionSecretProjection
= SmVersionSecretProjected { secret_resource: NonEmptyStr }
| SmVersionSecretNotAVersionResource { supplied: String }

fn sm_resolved_version_secret_resource(identity: SmResolvedVersionIdentity) -> SmVersionSecretProjection {
let text = identity as String
if !sm_resolved_version_identity_is_well_formed(name: text) {
SmVersionSecretNotAVersionResource { supplied: text }
} else {
match split(s: text, delimiter: "/versions/") |> first {
Present { value: secret_path } => SmVersionSecretProjected { secret_resource: secret_path as NonEmptyStr }
Absent => SmVersionSecretNotAVersionResource { supplied: text }
}
}
}

fn decode_sm_resolved_version_identity_wire(name: String) -> SmResolvedVersionIdentityDecodeOutcome {
if name.length() == 0 {
SmResolvedVersionIdentityDecodeRefused { cause: SmResolvedVersionIdentityEmpty }
Expand Down Expand Up @@ -281,6 +338,21 @@ fn decode_sm_access_version_wire_response(name: String, data_b64: String) -> SmA
// SECRET MANAGER OPERATION NOTES, hoisted here because annotations attach at
// module-item grain and a service body is a declaration body.
//
// GetSecret IS THE ONLY OPERATION HERE THAT DECLARES A RestOutcome, AND THE REASON IS ITS 404.
// Every operation in this service already declares 404 => GcpErrorShape, but a declared response arm
// is not a reachable value: extdeps.transports.rest records that dispatch_rest raises a rendered
// TypeError for any operation that does not declare an outcome field, so the status never reaches a
// caller. The wet run of 2026-09-06 measured it -- Secret Manager answered 404 for a printer access
// code and it arrived as TypeError { msg: "HTTP 404: ..." }, unreachable to the code that needed to
// act on it.
//
// WHY THIS OPERATION AND NOT THE WHOLE SERVICE AT ONCE: for AccessVersion a 404 is a failure -- the
// caller asked for a payload and there is none, and raising loses nothing a caller could have acted
// on. For GetSecret a 404 is THE ANSWER. Asking whether a container exists and being told it does
// not is a successful observation, and the one arm that must not throw is the one the question was
// asked to reach. Widening this to operations whose 404 nobody consumes would be edits with no
// consumer behind them; each opts in when a caller needs its status.
//
// GetSecretIamPolicy is the ONLY operation in this module that can settle what a
// secret's policy contains. It is the read half of the read-modify-write that
// setIamPolicy requires, and the only instrument here that can answer an ABSENCE
Expand Down Expand Up @@ -484,7 +556,7 @@ service gcp.SecretManager {

operation GetSecret {
input { access_token: Secret, project_id: GcpProjectId, secret: NonEmptyStr }
output { name: String, create_time: String from "createTime" }
output { name: String, create_time: String from "createTime", outcome: RestOutcome }
readonly
transport rest { method: GET, path: "/v1/projects/\{project_id\}/secrets/\{secret\}" }
response {
Expand Down
1 change: 1 addition & 0 deletions dag/extdeps/exec/command.dag
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,7 @@ fn argv_command(program: NonEmptyStr, arguments: List<String>) -> ArgvCommand
decl_ref(module_path: "extdeps.tools.hostname", decl_name: "hostname_short_read_command"),
decl_ref(module_path: "extdeps.tools.busybox", decl_name: "busybox_httpd_command"),
decl_ref(module_path: "extdeps.tools.busybox", decl_name: "busybox_tftpd_over_udpsvd_command"),
decl_ref(module_path: "extdeps.tools.curl", decl_name: "curl_ftps_upload_command"),
decl_ref(module_path: "extdeps.storage.nbd", decl_name: "nbd_server_command"),
decl_ref(module_path: "extdeps.storage.nbd", decl_name: "nbd_client_attach_command"),
decl_ref(module_path: "extdeps.storage.nbd", decl_name: "nbd_client_disconnect_command"),
Expand Down
148 changes: 148 additions & 0 deletions dag/extdeps/ietf/ftps.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,148 @@
module extdeps.ietf.ftps

import std.types { NonEmptyStr, Bool, Port }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
import extdeps.uri { Uri, Https }

// FTP OVER TLS, modeled because a device this repository owns speaks it and nothing here did.
//
// THE TWO NEGOTIATIONS ARE DIFFERENT PROTOCOLS WEARING ONE NAME, and conflating them is the
// failure this type exists to prevent. EXPLICIT FTPS connects in cleartext on the ordinary control
// port and issues AUTH TLS to upgrade. IMPLICIT FTPS expects TLS from the first byte on a separate
// port. A client that guesses wrong does not fail politely: an implicit server receives "AUTH TLS"
// as TLS garbage and drops the connection, while an explicit server receives a ClientHello as an
// unparseable command. Both surface as an unhelpful hangup, which is exactly the diagnostic that
// sends someone to check the password.
//
// THE TWO HALVES HAVE DIFFERENT AUTHORITIES, and an earlier draft of this module cited only the
// first for both. RFC 4217 standardises the EXPLICIT mechanism -- AUTH TLS over the normal control
// port -- and that is its whole subject; it neither defines implicit FTPS nor assigns it a port.
// The implicit form is not IETF-standardised at all: port 990 is an IANA service-name registration
// (ftps-data 989 / ftps 990), and the client behaviour this repository actually depends on is
// curl's, which treats the ftps:// scheme as TLS-from-the-first-byte. Citing the RFC for the
// implicit leg would attribute to a standards document a fact it does not contain, which is the
// nicknaming failure aimed at a source rather than at a symbol.
data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "www.rfc-editor.org/rfc/rfc4217"
}
}

data ftps_implicit_port_authority: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "www.iana.org/assignments/service-names-port-numbers/service-names-port-numbers.xhtml"
}
}

data ftps_implicit_client_behaviour_authority: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "curl.se/docs/url-syntax.html"
}
}

data extdeps_model_scope: ExternalModelScope = ExternalModelScope {
subject: ExternalSubjectRef {
declaration: DeclarationRef {
module_path: "extdeps.ietf.ftps",
decl_name: "FtpsNegotiation",
field: WholeDeclaration
}
},
first_citation: extdeps.ietf.ftps.extdeps_external_authority_anchor,
further_citations: [
extdeps.ietf.ftps.ftps_implicit_port_authority,
extdeps.ietf.ftps.ftps_implicit_client_behaviour_authority,
]
}

type FtpsNegotiation
= FtpsExplicit
| FtpsImplicit

// THE DEFAULT PORTS ARE PART OF THE NEGOTIATION, NOT A SEPARATE CHOICE. Explicit FTPS runs on the
// ordinary FTP control port because it BEGINS as ordinary FTP; implicit FTPS was assigned 990
// precisely so the server could know TLS was coming without being told. Deriving the port from the
// negotiation keeps a caller from pairing implicit with 21, which connects and then stalls.
// THE PORT IS std.types.Port, NOT A BARE Nat, AND THE ROUTE HERE IS WORTH RECORDING. A review asked
// for a marker on the bare Nat, noting in passing that no Port authority existed to consume. I wrote
// the marker on that basis WITHOUT CHECKING, and it was born stale: std.types.Port has been
// `Int where range(min: 1, max: 65535)` all along, consumed by boot artifact delivery, cli dispatch
// and three spark serving modules. A feature:/dissolve-on: whose trigger is already satisfied is
// worse than no marker -- it advertises a gap that is really an unconsumed authority, and it will be
// cited as evidence the question was considered.
//
// The lesson is the one this lane keeps relearning in a new costume: an ABSENCE is a census claim,
// and it is no more checkable when a reviewer supplies it than when I do. Nat admitted 0 and 70000,
// neither of which any endpoint can hold; Port refuses both by construction.
fn ftps_default_port(negotiation: FtpsNegotiation) -> Port {
match negotiation {
FtpsExplicit => 21
FtpsImplicit => 990
}
}

// WHAT TLS VERIFICATION IS ACTUALLY BEING GIVEN UP, NAMED FOR WHAT IT COSTS RATHER THAN FOR THE
// CERTIFICATE THAT PROMPTED IT. An earlier draft called the weakened arm FtpsAcceptSelfSigned, which
// reads as "trust THIS peer's own certificate" -- a scoped pin. It is not: the realization is curl's
// -k, which disables certificate-chain validation AND hostname verification together, so the
// connection will accept ANY certificate from ANY peer that answers on that address. That is not a
// pin, it is the absence of authentication, and a name that flatters it is the cosmetic-wrapper
// failure: the type would carry a distinction the realization does not enforce.
//
// THE REASON IS A PARAMETER OF THIS MODULE, NOT A ROSTER INSIDE IT. A free `because: NonEmptyStr`
// would let any consumer mint its own justification at the call site, which makes the weakening
// self-authorising -- so the reason must be a CLOSED class. But enumerating the admissible classes
// HERE was a layer inversion, and the note that stood in this place said so out loud without
// noticing: it argued that "adding a new excuse requires editing this module, where it is
// reviewable". That is admission control over which devices a CONSUMER FLEET may waive verification
// for, living inside a model of an IETF protocol.
//
// The tell was in the name. DeviceCertificateSubjectIsSerialNotAddress, and the measurement behind
// it, are an observation of THIS repository's printers -- and section 3 is explicit that
// observations produced here are receipts in the observing product layer, never facts owned by the
// observed upstream. A second fleet with a different device could not add its class without editing
// a protocol module it does not own, and adding one here would have widened the shape for everyone.
//
// So the protocol carries the SHAPE -- verification is on, or it is off for a reason of a type the
// consumer supplies -- and the consumer carries the closed roster of reasons it will admit. The
// weakening stays non-self-authorising because PeerClass is closed WHERE IT IS DECLARED; it simply
// is not declared here. One shape, N bound reason types.
//
// The honest ceiling of the weakened arm is mitigation, not a rung: the transfer stays confidential
// against a passive listener and remains fully open to an active one on the same LAN. Climbing it
// means pinning the peer's certificate or public key -- a scoped pin, verified -- which is a real
// construction rather than a rename, and is the trigger this arm is waiting on.
type FtpsPeerVerification<PeerClass>
= FtpsVerifyPeer
| FtpsPeerVerificationDisabled { peer: PeerClass }

fn ftps_verifies_peer<PeerClass>(v: FtpsPeerVerification<PeerClass>) -> Bool {
match v {
FtpsVerifyPeer => true
FtpsPeerVerificationDisabled { peer: _ } => false
}
}

type FtpsEndpoint<PeerClass> sole_constructor {
host: NonEmptyStr
port: Port
negotiation: FtpsNegotiation
verification: FtpsPeerVerification<PeerClass>
}

fn ftps_endpoint<PeerClass>(
host: NonEmptyStr,
negotiation: FtpsNegotiation,
verification: FtpsPeerVerification<PeerClass>,
) -> FtpsEndpoint<PeerClass> {
FtpsEndpoint {
host: host,
port: ftps_default_port(negotiation: negotiation),
negotiation: negotiation,
verification: verification,
}
}
Loading
Loading