Commit 746075c
Bump version to 0.4.5
Implements wiki ADR-040, ADR-041, ADR-042 — the implementer-facing
surface trio. With this release, foundation/uor-foundation-sdk fully
meets the needs of layer-3 ψ-pipeline implementors: closed-catalog
disambiguation of comparison semantics, type-system discrimination of
ψ-stage outputs, and a foundation-provided typed Rust verdict-envelope
surface.
ADR-040 — `type:LexicographicLessEqBound` (7th BoundShape individual):
- Adds the byte-sequence-comparison primitive to the closed BoundShape
catalog. Predicate form `observable(datum) <= bound` under canonical
big-endian unsigned ordering (lexicographic with shorter-prefix-rule
for variable-length).
- `LessEqBound` remains the integer-valued primitive (HammingMetric,
DerivationDepthObservable, etc.); `LexicographicLessEqBound` is the
byte-sequence-valued primitive paralleling it. Catalog declaration
alone determines comparison semantics — resolvers do not dispatch on
observable type.
- Ontology counts bump: INDIVIDUALS 3559 → 3560, CLASSIFICATION_PATH1
413 → 414, LEAN_CONSTANT_NAMESPACES 3422 → 3423.
ADR-041 — Typed-coordinate resolver carriers:
- Nine `#[repr(transparent)]` newtype wrappers over `&'a [u8]` —
`SimplicialComplexBytes`, `ChainComplexBytes`, `HomologyGroupsBytes`,
`BettiNumbersBytes`, `CochainComplexBytes`, `CohomologyGroupsBytes`,
`PostnikovTowerBytes`, `HomotopyGroupsBytes`, `KInvariantsBytes`
(the κ-label carrier). Each carrier is layout-identical to `&[u8]`;
the type wrapper is purely compile-time discrimination.
- The 8 ψ-stage resolver traits' `resolve` method now takes the prior
ψ-stage's typed carrier as input. `NerveResolver` retains `&[u8]`
input (the per-value bytes); the other seven receive their typed
predecessor-stage carrier. Cross-stage composition is type-checked
at compile time — mismatches surface as type errors at the resolver-
impl compile-time rather than runtime ShapeViolations.
- The catamorphism's resolver-bound fold-rules wrap `operand.bytes()`
in the typed carrier before invoking each downstream resolver.
- All 8 `Null<Category>Resolver` impls + 8 `NullResolverTuple` impls
updated to the new typed signatures.
ADR-042 — Inhabitance verdict typed Rust surface:
- `InhabitanceCertificateView<'a, T, Tag>` — `#[repr(transparent)]`
zero-allocation view over `&Grounded<T, Tag>` with accessors:
* `kappa_label() -> KInvariantsBytes<'_>` (the κ-label at ψ_9)
* `witness() -> WitnessValueTuple<'_>` (concrete witness)
* `certificate() -> &Validated<GroundingCertificate>`
* `certified_type() -> &'static str` (output IRI)
- `InhabitanceImpossibilityCertificate<'a>` — view over
`&PipelineFailure` with `contradiction_proof() -> &[u8]` accessor.
- `Grounded::as_inhabitance_certificate(&self)` and
`PipelineFailure::as_inhabitance_impossibility_certificate(&self)
-> Option<...>` as the accessor method surface.
- `inhabitance::dispatch_through_table(...)` helper for optional
`predicate:InhabitanceDispatchTable` consultation; three rule arms
(TwoSatDecider → HornSatDecider → ResidualVerdictResolver) routed
in ontology order via Option-returning closures.
- `WitnessValueTuple<'a>` + `WitnessTupleSource` trait — concrete
witness view backed by `Grounded`'s binding table.
- Universal: typed accessors available for any `Grounded<T, Tag>` /
`PipelineFailure`; applications whose admission relations are not
inhabitance questions simply don't call the typed accessors.
Implementer-verification end-to-end tests (uor-foundation-sdk/tests/smoke.rs):
- `adr041_typed_coordinate_carriers_are_repr_transparent_and_zero_cost`
— pins each typed carrier's `size_of` / `align_of` against `&[u8]`.
- `adr041_resolver_trait_signatures_type_check_psi_stage_composition`
— coerces every resolver trait's `resolve` method to its
wiki-mandated `fn`-pointer signature (regression-fence).
- `adr042_inhabitance_certificate_view_exposes_kappa_witness_certified_type`
— drives the canonical k-invariants branch through `Model::forward`,
borrows the `Grounded` as an `InhabitanceCertificateView`, asserts
the κ-label carries the chain markers, `certified_type` returns the
output IRI, and `witness` constructs.
- `adr042_inhabitance_impossibility_certificate_exposes_contradiction_proof`
— constructs a `ShapeViolation` failure, borrows as
`InhabitanceImpossibilityCertificate`, asserts `contradiction_proof`
surfaces the shape_iri bytes.
- `adr042_dispatch_through_table_routes_through_three_decider_arms`
— exercises all three rule-arm winners (TwoSatDecider, HornSatDecider,
ResidualVerdictResolver) through the dispatch helper.
- `adr040_lexicographic_less_eq_bound_is_in_closed_catalog`
— pins the foundation-emitted constant module's existence in scope.
All quality gates green: fmt, clippy --all-targets -D warnings,
workspace tests (57 SDK smoke tests, every foundation test), conformance
(544 passed, 0 failures, 10 meta-audit passed, 0 gaps detected).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>1 parent 33e868b commit 746075c
20 files changed
Lines changed: 1616 additions & 170 deletions
File tree
- codegen/src
- conformance
- standards
- foundation
- src
- user
- tests
- lean4
- UOR/Individuals
- spec/src
- namespaces
- uor-foundation-sdk/tests
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
18 | 18 | | |
19 | 19 | | |
20 | 20 | | |
21 | | - | |
| 21 | + | |
22 | 22 | | |
23 | 23 | | |
24 | 24 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
9 | 9 | | |
10 | 10 | | |
11 | 11 | | |
12 | | - | |
| 12 | + | |
13 | 13 | | |
14 | 14 | | |
15 | 15 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
6433 | 6433 | | |
6434 | 6434 | | |
6435 | 6435 | | |
| 6436 | + | |
| 6437 | + | |
| 6438 | + | |
| 6439 | + | |
| 6440 | + | |
| 6441 | + | |
| 6442 | + | |
| 6443 | + | |
| 6444 | + | |
| 6445 | + | |
| 6446 | + | |
| 6447 | + | |
| 6448 | + | |
| 6449 | + | |
| 6450 | + | |
| 6451 | + | |
| 6452 | + | |
6436 | 6453 | | |
6437 | 6454 | | |
6438 | 6455 | | |
| |||
0 commit comments