From 083aa899129315fad6f588bee67ab3581546c8e5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 00:00:44 -0400 Subject: [PATCH 1/4] =?UTF-8?q?WIP:=20T-26=20=E2=80=94=20std/=20boundary?= =?UTF-8?q?=20carriers:=20HttpMethod=20/=20Url=20/=20NetworkAddress=20(v4?= =?UTF-8?q?=20TAS?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/DECISIONS.md | 2 +- src/v4/STRUCTURE.md | 10 +++++++-- src/v4/extdeps/coordination.dag | 4 +++- src/v4/extdeps/formats/openapi.dag | 21 +++++------------- src/v4/std/network.dag | 34 ++++++++++++++++++++++++++++++ 5 files changed, 51 insertions(+), 20 deletions(-) create mode 100644 src/v4/std/network.dag diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index a0aaeb4e21f..956207848a8 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -477,7 +477,7 @@ the in-file `// coproduct dissolution β€” DECISIONS.md ` tag | **T-4.6-P4-OpenApiHeaderDeferredKey** | `OpenApiHeaderDeferredKey` | 🟑 | Header Object deferred members (style / explode / example / examples); excludes query-only **`allowEmptyValue`**; **`deprecated`** is **`OpenApiHeaderDeprecatedSlot`** on **`OpenApiHeaderObject`**; **`content`** is first-class on **`OpenApiHeaderPayloadSlot`** (XOR with **`schema`**). OAS Header churn on these deferrals β‡’ extend sum + row. | | **T-4.6-P4-OpenApiLinkDeferredKey** | `OpenApiLinkDeferredKey` | 🟑 | Link Object deferred members; Link spec churn β‡’ extend sum + row. | | **T-4.6-P4-OpenApiLinkTarget** | `OpenApiLinkTarget` | 🟑 | OAS Link Object **`operationId` XOR `operationRef`** β€” exactly one target identity; carried as `OpenApiLinkObject.target` (**T-4.6-OAS**). | -| **T-4.6-P4-OpenApiHttpMethod** | `OpenApiHttpMethod` | 🟒 | Closed eight-verb Operation map key set (OAS Path Item `get`…`trace`). | +| **T-4.6-P4-OpenApiHttpMethod** | `HttpMethod` from `std/network.dag` | 🟒 | Closed eight-verb Operation map key set (OAS Path Item `get`…`trace`) now consumes the shared T-26 carrier rather than a parallel OpenAPI enum. | | **T-4.6-P4-OpenApiOptionalString** | `OpenApiOptionalString` | 🟒 | Present/absent optional string field idiom over OAS optional strings. | | **T-4.6-P4-OpenApiHeaderRequiredSlot** | `OpenApiHeaderRequiredSlot` | 🟒 | Required boolean slot on Header Object (spec-bounded two-way). | | **T-4.6-P4-OpenApiHeaderDeprecatedSlot** | `OpenApiHeaderDeprecatedSlot` | 🟒 | Header Object **`deprecated`** optional boolean (Parameter-parity fixed field on **`OpenApiHeaderObject`**, **T-4.6-OAS**). | diff --git a/src/v4/STRUCTURE.md b/src/v4/STRUCTURE.md index 1ce42fb8cdc..160ef0c768f 100644 --- a/src/v4/STRUCTURE.md +++ b/src/v4/STRUCTURE.md @@ -16,7 +16,7 @@ src/v4/ TASKS.md # the XL task plan (count drift-proof; see T-15) DECISIONS.md # design-decisions ledger (RATIFIED + record) - std/ # substrate primitives (14 files) + std/ # substrate primitives (15 files) node.dag # 6 type connectives + 5 L1 behaviors (substrate root) algebra.dag # Magma/Monoid/BoolAlgebra/FreeMonoid (structures only) cardinality.dag # cardinality refinement, P4 decidability @@ -28,6 +28,7 @@ src/v4/ integer.dag # Int + fixed-width ints (Nat projected onto a width) float.dag # Float β€” IEEE-754 floating-point (rounding-aware algebra, not exact Field) text.dag # Char (Unicode code point) + String (FreeMonoid) + network.dag # HttpMethod / Url / NetworkAddress boundary carriers collection.dag # bounded containers verification.dag # TestClaim schema + TierΓ—Layer classification (v4-fresh; studied v3/dsl) report.dag # advisory carrier (NOT fail-closed Diagnostic); used by synthesis lens @@ -120,7 +121,7 @@ src/v4/ fixture/ # canonical input programs ``` -**Total: 69 .dag files + 5 docs + 5 .gitkeep = 79 files.** (Per invariant +**Total: 70 .dag files + 5 docs + 5 .gitkeep = 80 files.** (Per invariant #1 the enumeration above β€” not the count β€” is authoritative; the count is a checksum, updated on every operator-ratified file addition/removal. **Reconciliation (2026-05-17, PR #3225 / review #13750):** the prior printed @@ -132,6 +133,9 @@ intervening operator-ratified edits). **#3225** adds **`test/claim/manual/resolv extension (Option A, relay merry-ibex-337). βˆ’5 .dag 2026-05-15: work-direction meta-layer cut, operator-ratified. **2026-05-17 (PR #3212):** enumerate `test/claim/manual/*` (4) + `test/claim/impossible_bug/*` (6); checksum **65β†’69** `.dag`.) +**2026-05-18 (T-26):** add `std/network.dag` for shared +`HttpMethod` / `Url` / `NetworkAddress` boundary carriers; checksum +**69β†’70** `.dag`. ## Scalar/numeric concept decomposition @@ -151,6 +155,8 @@ by six concept-located files, each anchored to a real external concept inhabiting a rounding-aware algebra β€” *not* an exact `Field`, and *not* opaque: fully grounded, only its algebra is weakened) - `std/text.dag` β€” `Char` (Unicode code point) + `String` (`FreeMonoid`) +- `std/network.dag` β€” network boundary carriers (`HttpMethod`, `Url`, + `NetworkAddress`) shared by OpenAPI / coordination / wire contracts Each declares its own inhabitance (the inhabiting type owns its grounding β€” INVARIANTS P2); `algebra.dag` owns the algebra *structures* only. diff --git a/src/v4/extdeps/coordination.dag b/src/v4/extdeps/coordination.dag index 5f85c9050eb..b6a93478945 100644 --- a/src/v4/extdeps/coordination.dag +++ b/src/v4/extdeps/coordination.dag @@ -34,7 +34,7 @@ // - Effect types per coordination kind (HttpEffect / QueueEffect / StreamEffect / etc.) // // Consumes: -// - std/node.dag, std/diagnostic.dag, std/collection.dag +// - std/node.dag, std/diagnostic.dag, std/collection.dag, std/network.dag // - extdeps/languages/*.dag (per-endpoint language) // - extdeps/frameworks/*.dag (per-endpoint framework, optional) // @@ -45,3 +45,5 @@ module v4.extdeps.coordination + +import v4.std.network { NetworkAddress } diff --git a/src/v4/extdeps/formats/openapi.dag b/src/v4/extdeps/formats/openapi.dag index b4515e06e78..0441bb7ef5c 100644 --- a/src/v4/extdeps/formats/openapi.dag +++ b/src/v4/extdeps/formats/openapi.dag @@ -1,7 +1,7 @@ // src/v4/extdeps/formats/openapi.dag // Scope: OpenAPI 3.1.0 document slice; Lane C (TASKS.md T-4.6). -// Owns: OpenApiComponents, OpenApiComponentsDeferredKey, OpenApiComponentsMapKey, OpenApiComponentsPathItemsSlot, OpenApiComponentsSchemasSlot, OpenApiComponentsSlot, OpenApiContact, OpenApiContactSlot, OpenApiDocument, OpenApiDocumentRoot, OpenApiHeaderContentSingle, OpenApiHeaderDeferredKey, OpenApiHeaderDeprecatedSlot, OpenApiHeaderObject, OpenApiHeaderOrReference, OpenApiHeaderPayloadSlot, OpenApiHeaderRequiredSlot, OpenApiHeadersSlot, OpenApiHttpMethod, OpenApiInfo, OpenApiLicense, OpenApiLicenseSlot, OpenApiLicenseUrlOrIdentifierSlot, OpenApiLinkDeferredKey, OpenApiLinkObject, OpenApiLinkOrReference, OpenApiLinkTarget, OpenApiMediaType, OpenApiMediaTypeDeferredKey, OpenApiMediaTypeSchemaSlot, OpenApiOpenapiField3_1, OpenApiOpenapiObjectDeferredKey, OpenApiOperation, OpenApiOperationDeferredKey, OpenApiOptionalString, OpenApiPathItem, OpenApiPathItemDeferredKey, OpenApiPathItemOrReference, OpenApiPathTemplateKey, OpenApiPaths, OpenApiPathsSlot, OpenApiReferenceObject, OpenApiResponse, OpenApiResponseContentSlot, OpenApiResponseKey, OpenApiResponseKeyNonDefault, OpenApiResponseKeyWildcardKind, OpenApiResponseOrReference, OpenApiResponses, OpenApiResponsesDefaultSlot, OpenApiResponsesPrimaryEntry, OpenApiSchema, OpenApiSchemaOasMemberKey, OpenApiSpecificationExtensionKey, OpenApiStatusDigit, OpenApiStatusHundreds, OpenApiWebhooks, OpenApiWebhooksSlot -// Consumes: std/node.dag, std/diagnostic.dag, std/collection.dag, std/nat.dag, extdeps/formats/json_schema.dag, extdeps/formats/json.dag, extdeps/formats/yaml.dag +// Owns: OpenApiComponents, OpenApiComponentsDeferredKey, OpenApiComponentsMapKey, OpenApiComponentsPathItemsSlot, OpenApiComponentsSchemasSlot, OpenApiComponentsSlot, OpenApiContact, OpenApiContactSlot, OpenApiDocument, OpenApiDocumentRoot, OpenApiHeaderContentSingle, OpenApiHeaderDeferredKey, OpenApiHeaderDeprecatedSlot, OpenApiHeaderObject, OpenApiHeaderOrReference, OpenApiHeaderPayloadSlot, OpenApiHeaderRequiredSlot, OpenApiHeadersSlot, OpenApiInfo, OpenApiLicense, OpenApiLicenseSlot, OpenApiLicenseUrlOrIdentifierSlot, OpenApiLinkDeferredKey, OpenApiLinkObject, OpenApiLinkOrReference, OpenApiLinkTarget, OpenApiMediaType, OpenApiMediaTypeDeferredKey, OpenApiMediaTypeSchemaSlot, OpenApiOpenapiField3_1, OpenApiOpenapiObjectDeferredKey, OpenApiOperation, OpenApiOperationDeferredKey, OpenApiOptionalString, OpenApiPathItem, OpenApiPathItemDeferredKey, OpenApiPathItemOrReference, OpenApiPathTemplateKey, OpenApiPaths, OpenApiPathsSlot, OpenApiReferenceObject, OpenApiResponse, OpenApiResponseContentSlot, OpenApiResponseKey, OpenApiResponseKeyNonDefault, OpenApiResponseKeyWildcardKind, OpenApiResponseOrReference, OpenApiResponses, OpenApiResponsesDefaultSlot, OpenApiResponsesPrimaryEntry, OpenApiSchema, OpenApiSchemaOasMemberKey, OpenApiSpecificationExtensionKey, OpenApiStatusDigit, OpenApiStatusHundreds, OpenApiWebhooks, OpenApiWebhooksSlot +// Consumes: std/node.dag, std/diagnostic.dag, std/collection.dag, std/nat.dag, std/network.dag, extdeps/formats/json_schema.dag, extdeps/formats/json.dag, extdeps/formats/yaml.dag // Status: scaffold β€” TASKS.md T-4.6 // Anchor: https://spec.openapis.org/oas/v3.1.0 @@ -10,6 +10,7 @@ module v4.extdeps.formats.openapi import v4.extdeps.formats.json { JsonValue } import v4.extdeps.formats.json_schema { JsonSchema } +import v4.std.network { HttpMethod, Url } import v4.std.nat { Nat } @@ -106,18 +107,6 @@ type OpenApiSchema { } -// 🟒 coproduct dissolution β€” DECISIONS.md T-4.6-P4-OpenApiHttpMethod -type OpenApiHttpMethod - = OpenApiGet - | OpenApiPut - | OpenApiPost - | OpenApiDelete - | OpenApiOptions - | OpenApiHead - | OpenApiPatch - | OpenApiTrace - - // 🟒 coproduct dissolution β€” DECISIONS.md T-4.6-P4-OpenApiOptionalString type OpenApiOptionalString = OpenApiStringPresent { value: String } @@ -179,7 +168,7 @@ type OpenApiContactSlot // 🟑 coproduct dissolution β€” DECISIONS.md T-4.6-P4-OpenApiLicenseUrlOrIdentifierSlot type OpenApiLicenseUrlOrIdentifierSlot - = OpenApiLicenseUrlPresent { url: String } + = OpenApiLicenseUrlPresent { url: Url } | OpenApiLicenseIdentifierPresent { identifier: String } | OpenApiLicenseUrlOrIdentifierNeither @@ -356,7 +345,7 @@ type OpenApiOperation { type OpenApiPathItem { - routes: Map, + routes: Map, path_deferred_members: Map, path_specification_extensions: Map, } diff --git a/src/v4/std/network.dag b/src/v4/std/network.dag new file mode 100644 index 00000000000..d3090ccc376 --- /dev/null +++ b/src/v4/std/network.dag @@ -0,0 +1,34 @@ +// src/v4/std/network.dag +// Scope: network boundary carriers shared by transport, format, and coordination models. +// Anchor: RFC 9110 HTTP Semantics + RFC 5789 PATCH Method + RFC 3986 URI Generic Syntax +// Owns: HttpMethod, Url, NetworkAddress. +// Consumes: std text. +// Status: T-26 modeled. + + +module v4.std.network + + +import v4.std.text { String } + + +// RFC 9110 Section 9 method carrier, ported from dsl/std/types.dag. +type HttpMethod + = GET + | POST + | PUT + | PATCH + | DELETE + | HEAD + | OPTIONS + | TRACE + + +// Url: String refinement. Restore URI/URL parse predicate when the v4 +// refinement predicate substrate has a concrete pattern/format carrier. +type Url = String + + +type NetworkAddress { + url: Url, +} From 3210043dd4d240d842eb1ca62fc51f6b03cd8e42 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 00:03:47 -0400 Subject: [PATCH 2/4] T-26 std network boundary carriers --- src/v4/DECISIONS.md | 1 + src/v4/std/network.dag | 55 ++++++++++++++++++++++++++++++++++++------ 2 files changed, 48 insertions(+), 8 deletions(-) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 956207848a8..e6be46e55b4 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -88,6 +88,7 @@ remain boundary indexes until the named substrate support lands. | `std/logic.dag` | `Bool` | Green coproduct | Closed two-valued logic carrier: `True | False`. Terminal as the irreducible Boolean partition; Boolean algebra data is a structure over this carrier, not a second carrier. | | `std/text.dag` | `Char` | Yellow value-refinement scaffold | Documented: `Char = Nat` is an honest bridge carrier for Unicode scalar values because current substrate syntax cannot express `0..=0x10FFFF` excluding surrogate range `0xD800..=0xDFFF`. Bounded use: producers/ingesters must validate scalar-value membership. Trigger: bounded non-contiguous value refinement or equivalent character scalar carrier. | | `std/machine.dag` | `Byte`, `Word8`, `Word16`, `Word32`, `Word64`, `Word128` | Yellow fixed-cardinality scaffold | Documented: `bits: List` and `bytes: List` fields are intentionally unrefined list carriers. Bounded use: no consumer may treat list length as proven width without an explicit validator, witness, or grounding-side check. Trigger: fixed-cardinality list/field refinement substrate. | +| `std/network.dag` | `HttpMethod` (`T-26-HttpMethod`) | Green coproduct | RFC 9110 method token set plus RFC 5789 `PATCH`; closed boundary carrier consumed by OpenAPI / coordination / wire-contract models. | | `std/nat.dag` | `Nat` | Green coproduct | Closed Peano inductive natural number carrier: `Zero | Succ { prev: Nat }`. Terminal because the recursive structure is the natural-number definition; arithmetic data rows are structures over it. | | `std/node.dag` | `Connective`, `Behavior`, `NodeKind`, `EdgeLabel`, `EdgeDiscipline` | Green coproducts | `Connective` is the closed set of six type connectives; additions are substrate-extension stops. `Behavior` is the closed set of five L1 computation behaviors. `NodeKind` is the binary type/computation split. `EdgeLabel` is named vs positional child addressing. `EdgeDiscipline` is the closed classifier derived from connectives. | | `std/node.dag` | `Path` prior step sum | Green dissolved-away receipt | Positional path steps are deliberately dissolved: `Path` is `List` over named edges only. The removed path-step sum is not retained; positional addressing is subsumed by replacing the enclosing named subtree until a future ratified extension changes that shape. | diff --git a/src/v4/std/network.dag b/src/v4/std/network.dag index d3090ccc376..83d8ebd2434 100644 --- a/src/v4/std/network.dag +++ b/src/v4/std/network.dag @@ -1,7 +1,6 @@ // src/v4/std/network.dag -// Scope: network boundary carriers shared by transport, format, and coordination models. -// Anchor: RFC 9110 HTTP Semantics + RFC 5789 PATCH Method + RFC 3986 URI Generic Syntax -// Owns: HttpMethod, Url, NetworkAddress. +// Scope: network boundary carriers. +// Owns: HttpMethod, UriScheme, UriUserInfo, UriHost, UriPort, UriAuthority, UriPath, UriQuery, UriFragment, Url, NetworkAddress. // Consumes: std text. // Status: T-26 modeled. @@ -12,7 +11,8 @@ module v4.std.network import v4.std.text { String } -// RFC 9110 Section 9 method carrier, ported from dsl/std/types.dag. +// Anchor: https://www.rfc-editor.org/rfc/rfc9110.html#name-methods + https://www.rfc-editor.org/rfc/rfc5789.html +// 🟒 coproduct dissolution β€” DECISIONS.md T-26-HttpMethod type HttpMethod = GET | POST @@ -23,12 +23,51 @@ type HttpMethod | OPTIONS | TRACE +type UriScheme { + spelling: String, +} + +type UriUserInfo { + spelling: String, +} + +type UriHost { + spelling: String, +} + +type UriPort { + spelling: String, +} + +type UriAuthority { + userinfo: UriUserInfo, + host: UriHost, + port: UriPort, +} + +type UriPath { + spelling: String, +} + +type UriQuery { + spelling: String, +} + +type UriFragment { + spelling: String, +} -// Url: String refinement. Restore URI/URL parse predicate when the v4 -// refinement predicate substrate has a concrete pattern/format carrier. -type Url = String +// Anchor: https://www.rfc-editor.org/rfc/rfc3986.html#section-3 +type Url { + scheme: UriScheme, + authority: UriAuthority, + path: UriPath, + query: UriQuery, + fragment: UriFragment, +} +// Anchor: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2 type NetworkAddress { - url: Url, + authority: UriAuthority, } From 0d192cb92f44fb2cad19eef1dd75ec2ee64db043 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 00:09:40 -0400 Subject: [PATCH 3/4] T-26 std network boundary carriers --- src/v4/DECISIONS.md | 4 ++- src/v4/extdeps/formats/openapi.dag | 18 ++++++++-- src/v4/std/network.dag | 57 +++++++++++++++++++++++++++--- 3 files changed, 71 insertions(+), 8 deletions(-) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index e6be46e55b4..f7bc0650854 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -89,6 +89,8 @@ remain boundary indexes until the named substrate support lands. | `std/text.dag` | `Char` | Yellow value-refinement scaffold | Documented: `Char = Nat` is an honest bridge carrier for Unicode scalar values because current substrate syntax cannot express `0..=0x10FFFF` excluding surrogate range `0xD800..=0xDFFF`. Bounded use: producers/ingesters must validate scalar-value membership. Trigger: bounded non-contiguous value refinement or equivalent character scalar carrier. | | `std/machine.dag` | `Byte`, `Word8`, `Word16`, `Word32`, `Word64`, `Word128` | Yellow fixed-cardinality scaffold | Documented: `bits: List` and `bytes: List` fields are intentionally unrefined list carriers. Bounded use: no consumer may treat list length as proven width without an explicit validator, witness, or grounding-side check. Trigger: fixed-cardinality list/field refinement substrate. | | `std/network.dag` | `HttpMethod` (`T-26-HttpMethod`) | Green coproduct | RFC 9110 method token set plus RFC 5789 `PATCH`; closed boundary carrier consumed by OpenAPI / coordination / wire-contract models. | +| `std/network.dag` | `Rfc3986AbnfProduction`, `UriScheme`, `UriUserInfo`, `UriHost`, `UriPort`, `UriAuthority`, `UriPath`, `UriQuery`, `UriFragment`, `Url`, `NetworkAddress` | Green modeled facts | RFC 3986 Β§3 carriers model current-substrate facts now: `Url` is the component bundle; `UriAuthority` decomposes to userinfo/host/port; `UriPort` carries `Nat`; `UriScheme` carries a normalized spelling; every component carries its ABNF production data. | +| `std/network.dag` | RFC 3986 validated component refinements | Yellow `feature:T-25-core` scaffold | Residual only: fail-closed validation that a component spelling satisfies its carried ABNF production. Bounded use: constructors/ingesters must validate before constructing component values. Trigger: T-25-core base-type plus fail-closed validation shape and T-30 structural checker; dissolve under #3244 plan-binding by replacing producer-side convention with checked refinement witnesses. | | `std/nat.dag` | `Nat` | Green coproduct | Closed Peano inductive natural number carrier: `Zero | Succ { prev: Nat }`. Terminal because the recursive structure is the natural-number definition; arithmetic data rows are structures over it. | | `std/node.dag` | `Connective`, `Behavior`, `NodeKind`, `EdgeLabel`, `EdgeDiscipline` | Green coproducts | `Connective` is the closed set of six type connectives; additions are substrate-extension stops. `Behavior` is the closed set of five L1 computation behaviors. `NodeKind` is the binary type/computation split. `EdgeLabel` is named vs positional child addressing. `EdgeDiscipline` is the closed classifier derived from connectives. | | `std/node.dag` | `Path` prior step sum | Green dissolved-away receipt | Positional path steps are deliberately dissolved: `Path` is `List` over named edges only. The removed path-step sum is not retained; positional addressing is subsumed by replacing the enclosing named subtree until a future ratified extension changes that shape. | @@ -478,7 +480,7 @@ the in-file `// coproduct dissolution β€” DECISIONS.md ` tag | **T-4.6-P4-OpenApiHeaderDeferredKey** | `OpenApiHeaderDeferredKey` | 🟑 | Header Object deferred members (style / explode / example / examples); excludes query-only **`allowEmptyValue`**; **`deprecated`** is **`OpenApiHeaderDeprecatedSlot`** on **`OpenApiHeaderObject`**; **`content`** is first-class on **`OpenApiHeaderPayloadSlot`** (XOR with **`schema`**). OAS Header churn on these deferrals β‡’ extend sum + row. | | **T-4.6-P4-OpenApiLinkDeferredKey** | `OpenApiLinkDeferredKey` | 🟑 | Link Object deferred members; Link spec churn β‡’ extend sum + row. | | **T-4.6-P4-OpenApiLinkTarget** | `OpenApiLinkTarget` | 🟑 | OAS Link Object **`operationId` XOR `operationRef`** β€” exactly one target identity; carried as `OpenApiLinkObject.target` (**T-4.6-OAS**). | -| **T-4.6-P4-OpenApiHttpMethod** | `HttpMethod` from `std/network.dag` | 🟒 | Closed eight-verb Operation map key set (OAS Path Item `get`…`trace`) now consumes the shared T-26 carrier rather than a parallel OpenAPI enum. | +| **T-4.6-P4-OpenApiHttpMethod** | `OpenApiHttpMethod` | 🟒 | OAS Path Item operation field key set is the closed eight verbs `get`…`trace`; it intentionally excludes HTTP `CONNECT` even though shared `std/network.dag` `HttpMethod` includes it. | | **T-4.6-P4-OpenApiOptionalString** | `OpenApiOptionalString` | 🟒 | Present/absent optional string field idiom over OAS optional strings. | | **T-4.6-P4-OpenApiHeaderRequiredSlot** | `OpenApiHeaderRequiredSlot` | 🟒 | Required boolean slot on Header Object (spec-bounded two-way). | | **T-4.6-P4-OpenApiHeaderDeprecatedSlot** | `OpenApiHeaderDeprecatedSlot` | 🟒 | Header Object **`deprecated`** optional boolean (Parameter-parity fixed field on **`OpenApiHeaderObject`**, **T-4.6-OAS**). | diff --git a/src/v4/extdeps/formats/openapi.dag b/src/v4/extdeps/formats/openapi.dag index 0441bb7ef5c..5d3e0c8d2f5 100644 --- a/src/v4/extdeps/formats/openapi.dag +++ b/src/v4/extdeps/formats/openapi.dag @@ -1,6 +1,6 @@ // src/v4/extdeps/formats/openapi.dag // Scope: OpenAPI 3.1.0 document slice; Lane C (TASKS.md T-4.6). -// Owns: OpenApiComponents, OpenApiComponentsDeferredKey, OpenApiComponentsMapKey, OpenApiComponentsPathItemsSlot, OpenApiComponentsSchemasSlot, OpenApiComponentsSlot, OpenApiContact, OpenApiContactSlot, OpenApiDocument, OpenApiDocumentRoot, OpenApiHeaderContentSingle, OpenApiHeaderDeferredKey, OpenApiHeaderDeprecatedSlot, OpenApiHeaderObject, OpenApiHeaderOrReference, OpenApiHeaderPayloadSlot, OpenApiHeaderRequiredSlot, OpenApiHeadersSlot, OpenApiInfo, OpenApiLicense, OpenApiLicenseSlot, OpenApiLicenseUrlOrIdentifierSlot, OpenApiLinkDeferredKey, OpenApiLinkObject, OpenApiLinkOrReference, OpenApiLinkTarget, OpenApiMediaType, OpenApiMediaTypeDeferredKey, OpenApiMediaTypeSchemaSlot, OpenApiOpenapiField3_1, OpenApiOpenapiObjectDeferredKey, OpenApiOperation, OpenApiOperationDeferredKey, OpenApiOptionalString, OpenApiPathItem, OpenApiPathItemDeferredKey, OpenApiPathItemOrReference, OpenApiPathTemplateKey, OpenApiPaths, OpenApiPathsSlot, OpenApiReferenceObject, OpenApiResponse, OpenApiResponseContentSlot, OpenApiResponseKey, OpenApiResponseKeyNonDefault, OpenApiResponseKeyWildcardKind, OpenApiResponseOrReference, OpenApiResponses, OpenApiResponsesDefaultSlot, OpenApiResponsesPrimaryEntry, OpenApiSchema, OpenApiSchemaOasMemberKey, OpenApiSpecificationExtensionKey, OpenApiStatusDigit, OpenApiStatusHundreds, OpenApiWebhooks, OpenApiWebhooksSlot +// Owns: OpenApiComponents, OpenApiComponentsDeferredKey, OpenApiComponentsMapKey, OpenApiComponentsPathItemsSlot, OpenApiComponentsSchemasSlot, OpenApiComponentsSlot, OpenApiContact, OpenApiContactSlot, OpenApiDocument, OpenApiDocumentRoot, OpenApiHeaderContentSingle, OpenApiHeaderDeferredKey, OpenApiHeaderDeprecatedSlot, OpenApiHeaderObject, OpenApiHeaderOrReference, OpenApiHeaderPayloadSlot, OpenApiHeaderRequiredSlot, OpenApiHeadersSlot, OpenApiHttpMethod, OpenApiInfo, OpenApiLicense, OpenApiLicenseSlot, OpenApiLicenseUrlOrIdentifierSlot, OpenApiLinkDeferredKey, OpenApiLinkObject, OpenApiLinkOrReference, OpenApiLinkTarget, OpenApiMediaType, OpenApiMediaTypeDeferredKey, OpenApiMediaTypeSchemaSlot, OpenApiOpenapiField3_1, OpenApiOpenapiObjectDeferredKey, OpenApiOperation, OpenApiOperationDeferredKey, OpenApiOptionalString, OpenApiPathItem, OpenApiPathItemDeferredKey, OpenApiPathItemOrReference, OpenApiPathTemplateKey, OpenApiPaths, OpenApiPathsSlot, OpenApiReferenceObject, OpenApiResponse, OpenApiResponseContentSlot, OpenApiResponseKey, OpenApiResponseKeyNonDefault, OpenApiResponseKeyWildcardKind, OpenApiResponseOrReference, OpenApiResponses, OpenApiResponsesDefaultSlot, OpenApiResponsesPrimaryEntry, OpenApiSchema, OpenApiSchemaOasMemberKey, OpenApiSpecificationExtensionKey, OpenApiStatusDigit, OpenApiStatusHundreds, OpenApiWebhooks, OpenApiWebhooksSlot // Consumes: std/node.dag, std/diagnostic.dag, std/collection.dag, std/nat.dag, std/network.dag, extdeps/formats/json_schema.dag, extdeps/formats/json.dag, extdeps/formats/yaml.dag // Status: scaffold β€” TASKS.md T-4.6 // Anchor: https://spec.openapis.org/oas/v3.1.0 @@ -10,7 +10,7 @@ module v4.extdeps.formats.openapi import v4.extdeps.formats.json { JsonValue } import v4.extdeps.formats.json_schema { JsonSchema } -import v4.std.network { HttpMethod, Url } +import v4.std.network { Url } import v4.std.nat { Nat } @@ -107,6 +107,18 @@ type OpenApiSchema { } +// 🟒 coproduct dissolution β€” DECISIONS.md T-4.6-P4-OpenApiHttpMethod +type OpenApiHttpMethod + = OpenApiGet + | OpenApiPut + | OpenApiPost + | OpenApiDelete + | OpenApiOptions + | OpenApiHead + | OpenApiPatch + | OpenApiTrace + + // 🟒 coproduct dissolution β€” DECISIONS.md T-4.6-P4-OpenApiOptionalString type OpenApiOptionalString = OpenApiStringPresent { value: String } @@ -345,7 +357,7 @@ type OpenApiOperation { type OpenApiPathItem { - routes: Map, + routes: Map, path_deferred_members: Map, path_specification_extensions: Map, } diff --git a/src/v4/std/network.dag b/src/v4/std/network.dag index 83d8ebd2434..2aaa7ec74f1 100644 --- a/src/v4/std/network.dag +++ b/src/v4/std/network.dag @@ -1,7 +1,7 @@ // src/v4/std/network.dag // Scope: network boundary carriers. -// Owns: HttpMethod, UriScheme, UriUserInfo, UriHost, UriPort, UriAuthority, UriPath, UriQuery, UriFragment, Url, NetworkAddress. -// Consumes: std text. +// Owns: HttpMethod, Rfc3986AbnfProduction, UriScheme, UriUserInfo, UriHost, UriPort, UriAuthority, UriPath, UriQuery, UriFragment, Url, NetworkAddress. +// Consumes: std text, std nat. // Status: T-26 modeled. @@ -9,6 +9,7 @@ module v4.std.network import v4.std.text { String } +import v4.std.nat { Nat } // Anchor: https://www.rfc-editor.org/rfc/rfc9110.html#name-methods + https://www.rfc-editor.org/rfc/rfc5789.html @@ -21,22 +22,67 @@ type HttpMethod | DELETE | HEAD | OPTIONS + | CONNECT | TRACE +type Rfc3986AbnfProduction { + name: String, + expression: String, +} + +data rfc3986_scheme_abnf: Rfc3986AbnfProduction = Rfc3986AbnfProduction { + name: "scheme", + expression: "ALPHA *( ALPHA / DIGIT / plus / hyphen / dot )", +} + +data rfc3986_userinfo_abnf: Rfc3986AbnfProduction = Rfc3986AbnfProduction { + name: "userinfo", + expression: "*( unreserved / pct-encoded / sub-delims / colon )", +} + +data rfc3986_host_abnf: Rfc3986AbnfProduction = Rfc3986AbnfProduction { + name: "host", + expression: "IP-literal / IPv4address / reg-name", +} + +data rfc3986_port_abnf: Rfc3986AbnfProduction = Rfc3986AbnfProduction { + name: "port", + expression: "*DIGIT", +} + +data rfc3986_path_abnf: Rfc3986AbnfProduction = Rfc3986AbnfProduction { + name: "path", + expression: "path-abempty / path-absolute / path-noscheme / path-rootless / path-empty", +} + +data rfc3986_query_abnf: Rfc3986AbnfProduction = Rfc3986AbnfProduction { + name: "query", + expression: "*( pchar / slash / question )", +} + +data rfc3986_fragment_abnf: Rfc3986AbnfProduction = Rfc3986AbnfProduction { + name: "fragment", + expression: "*( pchar / slash / question )", +} + type UriScheme { - spelling: String, + normalized: String, + grammar: Rfc3986AbnfProduction, } type UriUserInfo { spelling: String, + grammar: Rfc3986AbnfProduction, } type UriHost { spelling: String, + grammar: Rfc3986AbnfProduction, } type UriPort { - spelling: String, + value: Nat, + grammar: Rfc3986AbnfProduction, } type UriAuthority { @@ -47,14 +93,17 @@ type UriAuthority { type UriPath { spelling: String, + grammar: Rfc3986AbnfProduction, } type UriQuery { spelling: String, + grammar: Rfc3986AbnfProduction, } type UriFragment { spelling: String, + grammar: Rfc3986AbnfProduction, } // Anchor: https://www.rfc-editor.org/rfc/rfc3986.html#section-3 From 49bfa518058687da6f404a9109b12a78615cbb0a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 00:39:48 -0400 Subject: [PATCH 4/4] T-26 std network boundary carriers --- src/v4/DECISIONS.md | 8 +++- src/v4/extdeps/formats/openapi.dag | 4 +- src/v4/std/network.dag | 59 ++++++++++++++++++++++++++---- 3 files changed, 60 insertions(+), 11 deletions(-) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index f7bc0650854..cdf3a5ffb21 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -89,7 +89,11 @@ remain boundary indexes until the named substrate support lands. | `std/text.dag` | `Char` | Yellow value-refinement scaffold | Documented: `Char = Nat` is an honest bridge carrier for Unicode scalar values because current substrate syntax cannot express `0..=0x10FFFF` excluding surrogate range `0xD800..=0xDFFF`. Bounded use: producers/ingesters must validate scalar-value membership. Trigger: bounded non-contiguous value refinement or equivalent character scalar carrier. | | `std/machine.dag` | `Byte`, `Word8`, `Word16`, `Word32`, `Word64`, `Word128` | Yellow fixed-cardinality scaffold | Documented: `bits: List` and `bytes: List` fields are intentionally unrefined list carriers. Bounded use: no consumer may treat list length as proven width without an explicit validator, witness, or grounding-side check. Trigger: fixed-cardinality list/field refinement substrate. | | `std/network.dag` | `HttpMethod` (`T-26-HttpMethod`) | Green coproduct | RFC 9110 method token set plus RFC 5789 `PATCH`; closed boundary carrier consumed by OpenAPI / coordination / wire-contract models. | -| `std/network.dag` | `Rfc3986AbnfProduction`, `UriScheme`, `UriUserInfo`, `UriHost`, `UriPort`, `UriAuthority`, `UriPath`, `UriQuery`, `UriFragment`, `Url`, `NetworkAddress` | Green modeled facts | RFC 3986 Β§3 carriers model current-substrate facts now: `Url` is the component bundle; `UriAuthority` decomposes to userinfo/host/port; `UriPort` carries `Nat`; `UriScheme` carries a normalized spelling; every component carries its ABNF production data. | +| `std/network.dag` | `Rfc3986AbnfProduction`, `UriScheme`, `UriUserInfo`, `UriUserInfoSlot`, `UriHost`, `UriPort`, `UriPortSlot`, `UriAuthority`, `UriPath`, `UriHierPart`, `UriQuery`, `UriQuerySlot`, `UriFragment`, `UriFragmentSlot`, `Url`, `UriRelativePart`, `UriRelativeReference`, `UriReference`, `NetworkAddress` | Green modeled facts | RFC 3986 Β§3/Β§4.1/Β§4.2 carriers model current-substrate facts now: `Url` is scheme + hier-part + optional query/fragment; `UriAuthority` decomposes to optional userinfo + host + optional port; `UriPort` carries `Nat`; `UriScheme` carries a normalized spelling; every component carries its ABNF production data; `UriReference` includes absolute and relative references for consumers such as OpenAPI URL fields. | +| `std/network.dag` | `UriUserInfoSlot`, `UriPortSlot`, `UriQuerySlot`, `UriFragmentSlot` (`T-26-UriComponentPresence`) | Green coproducts | RFC 3986 optional component presence is modeled structurally: userinfo, port, query, and fragment are present/absent slots, so constructors do not fabricate empty component values. | +| `std/network.dag` | `UriHierPart` (`T-26-UriHierPart`) | Green coproduct | RFC 3986 Β§3 hier-part alternatives are modeled as the closed choice among authority path, absolute path, rootless path, and empty path. | +| `std/network.dag` | `UriRelativePart` (`T-26-UriRelativePart`) | Green coproduct | RFC 3986 Β§4.2 relative-part alternatives are modeled as the closed choice among authority path, absolute path, no-scheme path, and empty path. | +| `std/network.dag` | `UriReference` (`T-26-UriReference`) | Green coproduct | RFC 3986 Β§4.1 URI-reference is the closed choice between an absolute URI and a relative reference; OpenAPI URL fields consume this carrier where relative references are permitted. | | `std/network.dag` | RFC 3986 validated component refinements | Yellow `feature:T-25-core` scaffold | Residual only: fail-closed validation that a component spelling satisfies its carried ABNF production. Bounded use: constructors/ingesters must validate before constructing component values. Trigger: T-25-core base-type plus fail-closed validation shape and T-30 structural checker; dissolve under #3244 plan-binding by replacing producer-side convention with checked refinement witnesses. | | `std/nat.dag` | `Nat` | Green coproduct | Closed Peano inductive natural number carrier: `Zero | Succ { prev: Nat }`. Terminal because the recursive structure is the natural-number definition; arithmetic data rows are structures over it. | | `std/node.dag` | `Connective`, `Behavior`, `NodeKind`, `EdgeLabel`, `EdgeDiscipline` | Green coproducts | `Connective` is the closed set of six type connectives; additions are substrate-extension stops. `Behavior` is the closed set of five L1 computation behaviors. `NodeKind` is the binary type/computation split. `EdgeLabel` is named vs positional child addressing. `EdgeDiscipline` is the closed classifier derived from connectives. | @@ -488,7 +492,7 @@ the in-file `// coproduct dissolution β€” DECISIONS.md ` tag | **T-4.6-P4-OpenApiHeaderOrReference** | `OpenApiHeaderOrReference` | 🟑 | Inline Header vs `$ref`; reference resolution + Reference Object parity triggers **T-4.6-OAS**. | | **T-4.6-P4-OpenApiLinkOrReference** | `OpenApiLinkOrReference` | 🟑 | Inline Link vs `$ref`; same reference substrate as **T-4.6-P4-OpenApiHeaderOrReference**. | | **T-4.6-P4-OpenApiContactSlot** | `OpenApiContactSlot` | 🟑 | Info Object `contact` optional subtree; OAS Contact Object churn β‡’ extend Contact fields + reconcile row. | -| **T-4.6-P4-OpenApiLicenseUrlOrIdentifierSlot** | `OpenApiLicenseUrlOrIdentifierSlot` | 🟑 | License Object `url` XOR `identifier` (+ neither) β€” mutual exclusion modeled; OAS License churn β‡’ amend row. | +| **T-4.6-P4-OpenApiLicenseUrlOrIdentifierSlot** | `OpenApiLicenseUrlOrIdentifierSlot` | 🟑 | License Object `url` XOR `identifier` (+ neither) β€” mutual exclusion modeled; `url` consumes `UriReference` because OAS URL fields admit relative references unless a field overrides that rule. OAS License churn β‡’ amend row. | | **T-4.6-P4-OpenApiLicenseSlot** | `OpenApiLicenseSlot` | 🟑 | Info `license` optional subtree; couples to **T-4.6-P4-OpenApiLicenseUrlOrIdentifierSlot**. | | **T-4.6-P4-OpenApiMediaTypeSchemaSlot** | `OpenApiMediaTypeSchemaSlot` | 🟑 | Media Type `schema` present vs absent; couples to `OpenApiSchema`. | | **T-4.6-P4-OpenApiResponseContentSlot** | `OpenApiResponseContentSlot` | 🟑 | Response `content` optional map; media-type map churn β‡’ amend modeling + row. | diff --git a/src/v4/extdeps/formats/openapi.dag b/src/v4/extdeps/formats/openapi.dag index 5d3e0c8d2f5..89e7087453e 100644 --- a/src/v4/extdeps/formats/openapi.dag +++ b/src/v4/extdeps/formats/openapi.dag @@ -10,7 +10,7 @@ module v4.extdeps.formats.openapi import v4.extdeps.formats.json { JsonValue } import v4.extdeps.formats.json_schema { JsonSchema } -import v4.std.network { Url } +import v4.std.network { UriReference } import v4.std.nat { Nat } @@ -180,7 +180,7 @@ type OpenApiContactSlot // 🟑 coproduct dissolution β€” DECISIONS.md T-4.6-P4-OpenApiLicenseUrlOrIdentifierSlot type OpenApiLicenseUrlOrIdentifierSlot - = OpenApiLicenseUrlPresent { url: Url } + = OpenApiLicenseUrlPresent { url: UriReference } | OpenApiLicenseIdentifierPresent { identifier: String } | OpenApiLicenseUrlOrIdentifierNeither diff --git a/src/v4/std/network.dag b/src/v4/std/network.dag index 2aaa7ec74f1..49a1bc6c923 100644 --- a/src/v4/std/network.dag +++ b/src/v4/std/network.dag @@ -1,6 +1,6 @@ // src/v4/std/network.dag // Scope: network boundary carriers. -// Owns: HttpMethod, Rfc3986AbnfProduction, UriScheme, UriUserInfo, UriHost, UriPort, UriAuthority, UriPath, UriQuery, UriFragment, Url, NetworkAddress. +// Owns: HttpMethod, Rfc3986AbnfProduction, UriScheme, UriUserInfo, UriUserInfoSlot, UriHost, UriPort, UriPortSlot, UriAuthority, UriPath, UriHierPart, UriQuery, UriQuerySlot, UriFragment, UriFragmentSlot, Url, UriRelativePart, UriRelativeReference, UriReference, NetworkAddress. // Consumes: std text, std nat. // Status: T-26 modeled. @@ -75,6 +75,11 @@ type UriUserInfo { grammar: Rfc3986AbnfProduction, } +// 🟒 coproduct dissolution β€” DECISIONS.md T-26-UriComponentPresence +type UriUserInfoSlot + = UriUserInfoAbsent + | UriUserInfoPresent { userinfo: UriUserInfo } + type UriHost { spelling: String, grammar: Rfc3986AbnfProduction, @@ -85,10 +90,15 @@ type UriPort { grammar: Rfc3986AbnfProduction, } +// 🟒 coproduct dissolution β€” DECISIONS.md T-26-UriComponentPresence +type UriPortSlot + = UriPortAbsent + | UriPortPresent { port: UriPort } + type UriAuthority { - userinfo: UriUserInfo, + userinfo: UriUserInfoSlot, host: UriHost, - port: UriPort, + port: UriPortSlot, } type UriPath { @@ -96,25 +106,60 @@ type UriPath { grammar: Rfc3986AbnfProduction, } +// 🟒 coproduct dissolution β€” DECISIONS.md T-26-UriHierPart +type UriHierPart + = UriHierAuthorityPath { authority: UriAuthority, path: UriPath } + | UriHierPathAbsolute { path: UriPath } + | UriHierPathRootless { path: UriPath } + | UriHierPathEmpty + type UriQuery { spelling: String, grammar: Rfc3986AbnfProduction, } +// 🟒 coproduct dissolution β€” DECISIONS.md T-26-UriComponentPresence +type UriQuerySlot + = UriQueryAbsent + | UriQueryPresent { query: UriQuery } + type UriFragment { spelling: String, grammar: Rfc3986AbnfProduction, } +// 🟒 coproduct dissolution β€” DECISIONS.md T-26-UriComponentPresence +type UriFragmentSlot + = UriFragmentAbsent + | UriFragmentPresent { fragment: UriFragment } + // Anchor: https://www.rfc-editor.org/rfc/rfc3986.html#section-3 type Url { scheme: UriScheme, - authority: UriAuthority, - path: UriPath, - query: UriQuery, - fragment: UriFragment, + hier_part: UriHierPart, + query: UriQuerySlot, + fragment: UriFragmentSlot, } +// Anchor: https://www.rfc-editor.org/rfc/rfc3986.html#section-4.2 +// 🟒 coproduct dissolution β€” DECISIONS.md T-26-UriRelativePart +type UriRelativePart + = UriRelativeAuthorityPath { authority: UriAuthority, path: UriPath } + | UriRelativePathAbsolute { path: UriPath } + | UriRelativePathNoScheme { path: UriPath } + | UriRelativePathEmpty + +type UriRelativeReference { + relative_part: UriRelativePart, + query: UriQuerySlot, + fragment: UriFragmentSlot, +} + +// 🟒 coproduct dissolution β€” DECISIONS.md T-26-UriReference +type UriReference + = UriReferenceAbsolute { uri: Url } + | UriReferenceRelative { relative: UriRelativeReference } + // Anchor: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2 type NetworkAddress {