Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
11 changes: 9 additions & 2 deletions src/v4/DECISIONS.md
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,13 @@ 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<Bit>` and `bytes: List<Byte>` 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`, `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. |
| `std/node.dag` | `Path` prior step sum | Green dissolved-away receipt | Positional path steps are deliberately dissolved: `Path` is `List<Symbol>` 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. |
Expand Down Expand Up @@ -591,15 +598,15 @@ the in-file `// <emoji> coproduct dissolution — DECISIONS.md <ID>` 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** | `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**). |
| **T-4.6-P4-OpenApiHeaderPayloadSlot** | `OpenApiHeaderPayloadSlot` | 🟡 | Header Object **`schema` XOR `content`** (OAS 3.1 mutual exclusion); **`content`** arm carries exactly one media-type entry via **`OpenApiHeaderContentSingle`** (**T-4.6-OAS**). |
| **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. |
Expand Down
14 changes: 11 additions & 3 deletions src/v4/STRUCTURE.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 landed + 1 P2-staging witness; see note on `fact_density.dag`)
std/ # substrate primitives (15 landed + 1 P2-staging witness; see note on `fact_density.dag`)
node.dag # 6 type connectives + 5 L1 behaviors (substrate root)
algebra.dag # Magma/Monoid/BoolAlgebra/FreeMonoid (structures only)
cardinality.dag # cardinality refinement, P4 decidability
Expand All @@ -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<Char>)
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
Expand Down Expand Up @@ -122,7 +123,7 @@ src/v4/
fixture/ # canonical input programs
```

**Total: 70 .dag files + 5 docs + 5 .gitkeep = 80 files.** (Per invariant
**Total: 72 .dag files + 5 docs + 5 .gitkeep = 82 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
Expand All @@ -134,8 +135,13 @@ 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`.
**2026-05-18 (T-29):** add `extdeps/cpp_abi.dag` for the operator-ratified
C++ ABI / target data-model feeder; checksum **69→70** `.dag`.
C++ ABI / target data-model feeder; checksum **70→71** `.dag`.
**2026-05-18 (T-30):** add `std/fact_density.dag` P2-staging parse witness;
checksum **71→72** `.dag`.

## Scalar/numeric concept decomposition

Expand All @@ -155,6 +161,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<Char>`)
- `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.
Expand Down
10 changes: 3 additions & 7 deletions src/v4/extdeps/coordination.dag
Original file line number Diff line number Diff line change
@@ -1,20 +1,16 @@
// src/v4/extdeps/coordination.dag
// Scope: Multi-program coordination as effect-typed Bind composition.
// Owns: NetworkAddress, LanguageRef, FrameworkRef, FrameworkBinding, EndpointRef, Endpoint, SettleBound, ConvergeBound, ExchangePattern, SettlementGuarantee, ConsistencyGuarantee, CoordinationEffectKind, BindRef, CoordinationBind, WireContractFacts, WireContract, DeploymentUnit.
// Consumes: std/node.dag, std/collection.dag, std/nat.dag.
// Owns: LanguageRef, FrameworkRef, FrameworkBinding, EndpointRef, Endpoint, SettleBound, ConvergeBound, ExchangePattern, SettlementGuarantee, ConsistencyGuarantee, CoordinationEffectKind, BindRef, CoordinationBind, WireContractFacts, WireContract, DeploymentUnit.
// Consumes: std/node.dag, std/collection.dag, std/nat.dag, std/network.dag.
// Status: Modeled with tracked scaffolds.

module v4.extdeps.coordination

import v4.std.collection { List }
import v4.std.nat { Nat }
import v4.std.network { NetworkAddress }
import v4.std.node { Symbol }

// Anchor: RFC 3986, January 2005, https://www.rfc-editor.org/rfc/rfc3986
type NetworkAddress {
identity: Symbol
}

type LanguageRef {
identity: Symbol
}
Expand Down
5 changes: 3 additions & 2 deletions src/v4/extdeps/formats/openapi.dag
Original file line number Diff line number Diff line change
@@ -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
// 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

Expand All @@ -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 { UriReference }
import v4.std.nat { Nat }


Expand Down Expand Up @@ -179,7 +180,7 @@ type OpenApiContactSlot

// 🟡 coproduct dissolution — DECISIONS.md T-4.6-P4-OpenApiLicenseUrlOrIdentifierSlot
type OpenApiLicenseUrlOrIdentifierSlot
= OpenApiLicenseUrlPresent { url: String }
= OpenApiLicenseUrlPresent { url: UriReference }
| OpenApiLicenseIdentifierPresent { identifier: String }
| OpenApiLicenseUrlOrIdentifierNeither

Expand Down
167 changes: 167 additions & 0 deletions src/v4/std/network.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,167 @@
// src/v4/std/network.dag
// Scope: network boundary carriers.
// 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.


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
// 🟢 coproduct dissolution — DECISIONS.md T-26-HttpMethod
type HttpMethod
= GET
| POST
| PUT
| PATCH
| 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 {
normalized: String,
grammar: Rfc3986AbnfProduction,
}

type UriUserInfo {
spelling: String,
grammar: Rfc3986AbnfProduction,
}

// 🟢 coproduct dissolution — DECISIONS.md T-26-UriComponentPresence
type UriUserInfoSlot
= UriUserInfoAbsent
| UriUserInfoPresent { userinfo: UriUserInfo }

type UriHost {
spelling: String,
grammar: Rfc3986AbnfProduction,
}

type UriPort {
value: Nat,
grammar: Rfc3986AbnfProduction,
}

// 🟢 coproduct dissolution — DECISIONS.md T-26-UriComponentPresence
type UriPortSlot
= UriPortAbsent
| UriPortPresent { port: UriPort }

type UriAuthority {
userinfo: UriUserInfoSlot,
host: UriHost,
port: UriPortSlot,
}

type UriPath {
spelling: String,
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,
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 {
authority: UriAuthority,
}
Loading