Commit 1420c6d
Bump version to 0.4.13
Implements wiki ADR-057 (Bounded recursive structural typing via
ConstraintRef::Recurse + foundation shape-IRI registry).
The framework's constraint vocabulary now admits bounded recursive
shape references — the structural analog of `Term::Recurse` at the
constraint level. Applications carrying inductively-defined input
domains (JSON values, XML documents, AST shapes, S-expressions, ASN.1 /
Protobuf message families, filesystem hierarchies, rose trees) can
declare their typed structural form at the constraint-geometry level
through `ConstraintRef::Recurse { shape_iri, descent_bound }` without
hitting the const-eval barrier that direct self-reference in
`partition_coproduct!`'s operand list raises.
Foundation surface additions:
- `ConstraintRef::Recurse { shape_iri: &'static str, descent_bound: u32 }`
variant on `pipeline::ConstraintRef` + parallel `LeafConstraintRef::Recurse`
+ `ConstraintRef::as_leaf()` arm + `LeafConstraintRef::into_constraint()` arm.
- `pipeline::shape_iri_registry::RegisteredShape { iri, site_count,
constraints, cycle_size }` mirror struct.
- `pipeline::shape_iri_registry::lookup_shape(iri) -> Option<&'static
RegisteredShape>` runtime lookup surface for ψ_1 NerveResolver.
- `pipeline::shape_iri_registry::__register_shape(...)` doc-hidden entry
point for the SDK `register_shape!` macro and dynamic loaders.
- `shift_constraint` / `shift_leaf_constraint` arms pass Recurse through
unchanged (no site references to shift).
- `encode_constraint_to_clauses` returns `Some(EMPTY)` for Recurse
(preflight feasibility deferred to runtime ψ_1 NerveResolver).
- `validate_constrained_type_const` accepts Recurse on non-empty
shape_iri (registry lookup happens at runtime, parallel to
ADR-049's LandauerCost deferral).
- `validate_coproduct_structure` (ST_6/ST_7/ST_8 walker) passes Recurse
through (no site references at this level).
Wire-format integration per ADR-013/TR-08:
- `fold_constraint_ref` emits discriminant byte 10 for Recurse (after
Conjunction = 9), with payload `shape_iri | 0x00 | descent_bound`.
- `TRACE_REPLAY_FORMAT_VERSION` bumped 9 → 10.
- `rust/trace_byte_layout_pinned` validator updated.
Audit surfaces:
- foundation/tests/public-api.snapshot + .nostd: add
`mod shape_iri_registry`.
- conformance/endpoint_coverage.toml: ADR-057 coverage mapping.
Conformance test coverage (foundation/tests/behavior_adr_057_recursive_typing.rs):
- constraint_ref_recurse_variant_carries_shape_iri_and_descent_bound
- leaf_constraint_ref_recurse_round_trips_via_as_leaf_into_constraint
- shift_constraint_passes_recurse_through_unchanged
- shift_leaf_constraint_passes_recurse_through_unchanged
- shape_iri_registry_registered_shape_carries_canonical_fields
- shape_iri_registry_lookup_returns_none_for_unregistered_iri
- fold_constraint_ref_emits_discriminant_byte_10_for_recurse
Future work (not blocking this release; ADR-057 surface is in place):
- SDK `register_shape!` macro emitting link-section registration entries
feeding `FOUNDATION_REGISTRY`. The doc-hidden `__register_shape` entry
point is in place; the link-section collection mechanism extends
`FOUNDATION_REGISTRY` in a follow-up release.
- `partition_coproduct!` / `partition_product!` `recurse:T` /
`recurse(<bound>):T` operand-grammar extension lowering to
Recurse-bearing CONSTRAINTS arrays. The runtime substrate is in place;
the SDK convenience comes in a follow-up.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>1 parent 1a70b43 commit 1420c6d
16 files changed
Lines changed: 579 additions & 54 deletions
File tree
- codegen/src
- conformance
- shapes
- src/validators/rust
- foundation
- src
- tests
- lean4
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 | |
|---|---|---|---|
| |||
5440 | 5440 | | |
5441 | 5441 | | |
5442 | 5442 | | |
5443 | | - | |
| 5443 | + | |
5444 | 5444 | | |
5445 | 5445 | | |
5446 | 5446 | | |
| |||
5934 | 5934 | | |
5935 | 5935 | | |
5936 | 5936 | | |
| 5937 | + | |
| 5938 | + | |
| 5939 | + | |
| 5940 | + | |
| 5941 | + | |
| 5942 | + | |
| 5943 | + | |
| 5944 | + | |
| 5945 | + | |
5937 | 5946 | | |
5938 | 5947 | | |
5939 | 5948 | | |
| |||
13155 | 13164 | | |
13156 | 13165 | | |
13157 | 13166 | | |
13158 | | - | |
| 13167 | + | |
| 13168 | + | |
| 13169 | + | |
| 13170 | + | |
13159 | 13171 | | |
13160 | 13172 | | |
13161 | 13173 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1601 | 1601 | | |
1602 | 1602 | | |
1603 | 1603 | | |
| 1604 | + | |
| 1605 | + | |
| 1606 | + | |
| 1607 | + | |
| 1608 | + | |
| 1609 | + | |
| 1610 | + | |
| 1611 | + | |
| 1612 | + | |
| 1613 | + | |
| 1614 | + | |
| 1615 | + | |
| 1616 | + | |
| 1617 | + | |
| 1618 | + | |
| 1619 | + | |
1604 | 1620 | | |
1605 | 1621 | | |
1606 | 1622 | | |
| |||
1636 | 1652 | | |
1637 | 1653 | | |
1638 | 1654 | | |
| 1655 | + | |
| 1656 | + | |
| 1657 | + | |
| 1658 | + | |
| 1659 | + | |
1639 | 1660 | | |
1640 | 1661 | | |
1641 | 1662 | | |
| |||
1672 | 1693 | | |
1673 | 1694 | | |
1674 | 1695 | | |
| 1696 | + | |
| 1697 | + | |
| 1698 | + | |
1675 | 1699 | | |
1676 | 1700 | | |
1677 | 1701 | | |
| |||
1701 | 1725 | | |
1702 | 1726 | | |
1703 | 1727 | | |
| 1728 | + | |
| 1729 | + | |
| 1730 | + | |
1704 | 1731 | | |
1705 | 1732 | | |
1706 | 1733 | | |
| |||
1759 | 1786 | | |
1760 | 1787 | | |
1761 | 1788 | | |
| 1789 | + | |
| 1790 | + | |
| 1791 | + | |
| 1792 | + | |
| 1793 | + | |
| 1794 | + | |
1762 | 1795 | | |
1763 | 1796 | | |
1764 | 1797 | | |
| |||
2041 | 2074 | | |
2042 | 2075 | | |
2043 | 2076 | | |
| 2077 | + | |
| 2078 | + | |
| 2079 | + | |
| 2080 | + | |
| 2081 | + | |
| 2082 | + | |
| 2083 | + | |
| 2084 | + | |
| 2085 | + | |
| 2086 | + | |
| 2087 | + | |
| 2088 | + | |
| 2089 | + | |
| 2090 | + | |
| 2091 | + | |
| 2092 | + | |
| 2093 | + | |
| 2094 | + | |
| 2095 | + | |
| 2096 | + | |
| 2097 | + | |
| 2098 | + | |
| 2099 | + | |
| 2100 | + | |
| 2101 | + | |
| 2102 | + | |
| 2103 | + | |
| 2104 | + | |
| 2105 | + | |
| 2106 | + | |
| 2107 | + | |
| 2108 | + | |
| 2109 | + | |
| 2110 | + | |
| 2111 | + | |
| 2112 | + | |
| 2113 | + | |
| 2114 | + | |
| 2115 | + | |
| 2116 | + | |
| 2117 | + | |
| 2118 | + | |
| 2119 | + | |
| 2120 | + | |
| 2121 | + | |
| 2122 | + | |
| 2123 | + | |
| 2124 | + | |
| 2125 | + | |
| 2126 | + | |
| 2127 | + | |
| 2128 | + | |
| 2129 | + | |
| 2130 | + | |
| 2131 | + | |
| 2132 | + | |
| 2133 | + | |
| 2134 | + | |
| 2135 | + | |
| 2136 | + | |
| 2137 | + | |
| 2138 | + | |
| 2139 | + | |
| 2140 | + | |
| 2141 | + | |
| 2142 | + | |
| 2143 | + | |
| 2144 | + | |
| 2145 | + | |
| 2146 | + | |
| 2147 | + | |
| 2148 | + | |
| 2149 | + | |
| 2150 | + | |
| 2151 | + | |
| 2152 | + | |
| 2153 | + | |
| 2154 | + | |
| 2155 | + | |
| 2156 | + | |
| 2157 | + | |
| 2158 | + | |
| 2159 | + | |
| 2160 | + | |
| 2161 | + | |
| 2162 | + | |
| 2163 | + | |
| 2164 | + | |
| 2165 | + | |
| 2166 | + | |
| 2167 | + | |
| 2168 | + | |
| 2169 | + | |
| 2170 | + | |
| 2171 | + | |
| 2172 | + | |
| 2173 | + | |
| 2174 | + | |
| 2175 | + | |
| 2176 | + | |
| 2177 | + | |
| 2178 | + | |
2044 | 2179 | | |
2045 | 2180 | | |
2046 | 2181 | | |
| |||
6013 | 6148 | | |
6014 | 6149 | | |
6015 | 6150 | | |
| 6151 | + | |
| 6152 | + | |
| 6153 | + | |
| 6154 | + | |
| 6155 | + | |
6016 | 6156 | | |
6017 | 6157 | | |
6018 | 6158 | | |
| |||
6082 | 6222 | | |
6083 | 6223 | | |
6084 | 6224 | | |
| 6225 | + | |
| 6226 | + | |
| 6227 | + | |
| 6228 | + | |
| 6229 | + | |
6085 | 6230 | | |
6086 | 6231 | | |
6087 | 6232 | | |
| |||
6254 | 6399 | | |
6255 | 6400 | | |
6256 | 6401 | | |
| 6402 | + | |
| 6403 | + | |
| 6404 | + | |
| 6405 | + | |
| 6406 | + | |
6257 | 6407 | | |
6258 | 6408 | | |
6259 | 6409 | | |
| |||
6903 | 7053 | | |
6904 | 7054 | | |
6905 | 7055 | | |
| 7056 | + | |
| 7057 | + | |
| 7058 | + | |
| 7059 | + | |
| 7060 | + | |
6906 | 7061 | | |
6907 | 7062 | | |
6908 | 7063 | | |
| |||
0 commit comments