Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
66 commits
Select commit Hold shift + click to select a range
bb643bc
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
84a476d
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
91e7d4a
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
ede338d
cargo fmt: stage0 emit and ownership_wrap tests.
Jul 26, 2026
3f49164
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
91baceb
Align value-site Rc wrap with rendered return types for regen.
Jul 26, 2026
da1f09d
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
5b97d86
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
a8097dc
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
2b809eb
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
51dd961
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
3d58454
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
4d0b886
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
2301970
Address PR #7223 review: fail-closed catalog row realization + parse …
Jul 26, 2026
a1a577f
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
a427a5c
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
14e4214
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
f10ac7d
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
0f18cde
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
fce9565
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
7de6fc5
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
6c36430
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
b41cd8c
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
0bb677d
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
637ad2e
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
7ee76d6
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
8dfd600
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
f0e9db7
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
9c78466
Revert broken stage0 regen that broke v1-compiler build.
Jul 26, 2026
f017769
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
a8b8fb8
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
02ea439
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
d94744a
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
4c1a503
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
d692748
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
775e24f
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
19f6832
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
48aa1c0
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
cb3926d
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
c45339f
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
23ac7ae
Revert broken stage0 regen that broke v1-compiler build.
Jul 26, 2026
de41ebb
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
9d60985
Fix rust_sg_rc_wrap_layer_lookup fold to preserve accumulator on miss.
Jul 26, 2026
5a759d1
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
4af0840
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
e21d8c9
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
70e5fae
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
6e0f4be
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
2dcfbdb
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
0917cb8
Revert "WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + …
Jul 26, 2026
fd56a57
chore: re-trigger modeling-coherence after reverting oversized stage0…
Jul 26, 2026
a3287d4
Merge remote-tracking branch 'origin/main' into session/witty-wolf-28…
Jul 26, 2026
1cde8b1
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
1bec537
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
715210e
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
39d387c
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
a6079f3
Fail-closed v1 wrap lookup when enrolled carrier has no catalog row.
Jul 26, 2026
73a232b
cargo fmt after SeedWrapOutcome fail-closed refactor.
Jul 26, 2026
54836e8
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
183308e
Derive v2 wrap-catalog projection from row-key coproduct (review 43418).
Jul 26, 2026
32960a3
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
fe38319
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
773c09b
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
0183a98
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 2026
7773fe1
fix(ownership-68): route inferred wrap checks through catalog use sites
Jul 26, 2026
cc21b2a
WIP: E0308 mechanical trio: Range-vs-usize + String-vs-str + Unit-vs-…
Jul 26, 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
4 changes: 2 additions & 2 deletions dag/extdeps/languages/rust/emit.dag
Original file line number Diff line number Diff line change
Expand Up @@ -158,8 +158,8 @@ data rust_lambda_template: String = "|{0}| {1}"

data rust_error_expr_template: String = "panic!({0})"

data rust_list_literal_empty: String = "Rc::new(vec![])"
data rust_list_literal_template: String = "Rc::new(vec![{0}])"
data rust_list_literal_empty: String = "vec![]"
data rust_list_literal_template: String = "vec![{0}]"

data rust_null_coalesce_template: String = "{0}.unwrap_or_else(|| {1})"

Expand Down
255 changes: 255 additions & 0 deletions dag/extdeps/languages/rust/wrap_catalog.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,255 @@
module extdeps.languages.rust.wrap_catalog

data rust_sg_rc_wrap_catalog_note: String = "Single authority for rust_sg_rc_use_site_ownership_catalog rows (v1 seed emitter + v2.extdeps.languages.rust). Carrier is a closed enum (not a string tag). NonEmptyDiagnostics aliases Diagnostics at the lookup boundary only — dissolve-on: modeled alias row in the catalog when NonEmptyDiagnostics itself dissolves (§3 nickname; do not grow rust_sg_rc_wrap_carrier_key string branches)."

data rust_sg_rc_wrap_catalog_realization_fork_note: String = "Stage0 seed hand-sync (OWNERSHIP-68): extdeps_languages_rust_wrap_catalog.rs carries OwnershipWrapCatalogRowKey rows — same closed enum as this module. Stale full-regen emit still materializes carrier: String until compile-green self-host regen lands. Dissolve-on: regen_verify green without string-carrier rows (sharp-bee-290 Gate 3 / ROADMAP.md §④ regen_verify + rc-ownership-wrap-decision-design.md step 3)."

type OwnershipWrapUseSite
= OwnershipWrapUseSiteAbsent
| OwnershipAtFunctionReturn
| OwnershipAtFunctionParameter
| OwnershipAtStructField
| OwnershipAtBindingProjection

type OwnershipReferenceLayer
= ReferenceLayerOwned
| ReferenceLayerRc
| ReferenceLayerBox

type OwnershipWrapSourceProjection
= UseSiteOwnershipExactCarrier
| UseSiteOwnershipInstantiationHeadCarrier

type OwnershipWrapCarrier
= WrapCarrierDiagnostics
| WrapCarrierNode
| WrapCarrierTestClaim
| WrapCarrierFreeMonoid
| WrapCarrierOutcome
| WrapCarrierModelCore
| WrapCarrierAlgebraInhabitanceDecl
| WrapCarrierProbeHeap
| WrapCarrierUseSiteVerdict

type OwnershipWrapCatalogRowKey
= WrapRowDiagnosticsReturn
| WrapRowDiagnosticsParam
| WrapRowDiagnosticsBinding
| WrapRowNodeReturn
| WrapRowNodeParam
| WrapRowNodeStructField
| WrapRowNodeBinding
| WrapRowTestClaimReturn
| WrapRowTestClaimBinding
| WrapRowFreeMonoidReturn
| WrapRowFreeMonoidBinding
| WrapRowOutcomeReturn
| WrapRowOutcomeBinding
| WrapRowModelCoreReturn
| WrapRowModelCoreBinding
| WrapRowAlgebraInhabitanceReturn
| WrapRowAlgebraInhabitanceBinding
| WrapRowProbeHeapReturn
| WrapRowProbeHeapBinding
| WrapRowUseSiteVerdictReturn
| WrapRowUseSiteVerdictParam
| WrapRowUseSiteVerdictBinding

fn rust_sg_rc_wrap_catalog_row_carrier(key: OwnershipWrapCatalogRowKey) -> OwnershipWrapCarrier {
match key {
WrapRowDiagnosticsReturn => WrapCarrierDiagnostics
WrapRowDiagnosticsParam => WrapCarrierDiagnostics
WrapRowDiagnosticsBinding => WrapCarrierDiagnostics
WrapRowNodeReturn => WrapCarrierNode
WrapRowNodeParam => WrapCarrierNode
WrapRowNodeStructField => WrapCarrierNode
WrapRowNodeBinding => WrapCarrierNode
WrapRowTestClaimReturn => WrapCarrierTestClaim
WrapRowTestClaimBinding => WrapCarrierTestClaim
WrapRowFreeMonoidReturn => WrapCarrierFreeMonoid
WrapRowFreeMonoidBinding => WrapCarrierFreeMonoid
WrapRowOutcomeReturn => WrapCarrierOutcome
WrapRowOutcomeBinding => WrapCarrierOutcome
WrapRowModelCoreReturn => WrapCarrierModelCore
WrapRowModelCoreBinding => WrapCarrierModelCore
WrapRowAlgebraInhabitanceReturn => WrapCarrierAlgebraInhabitanceDecl
WrapRowAlgebraInhabitanceBinding => WrapCarrierAlgebraInhabitanceDecl
WrapRowProbeHeapReturn => WrapCarrierProbeHeap
WrapRowProbeHeapBinding => WrapCarrierProbeHeap
WrapRowUseSiteVerdictReturn => WrapCarrierUseSiteVerdict
WrapRowUseSiteVerdictParam => WrapCarrierUseSiteVerdict
WrapRowUseSiteVerdictBinding => WrapCarrierUseSiteVerdict
}
}

fn rust_sg_rc_wrap_catalog_row_use_site(key: OwnershipWrapCatalogRowKey) -> OwnershipWrapUseSite {
match key {
WrapRowDiagnosticsReturn => OwnershipAtFunctionReturn
WrapRowNodeReturn => OwnershipAtFunctionReturn
WrapRowTestClaimReturn => OwnershipAtFunctionReturn
WrapRowFreeMonoidReturn => OwnershipAtFunctionReturn
WrapRowOutcomeReturn => OwnershipAtFunctionReturn
WrapRowModelCoreReturn => OwnershipAtFunctionReturn
WrapRowAlgebraInhabitanceReturn => OwnershipAtFunctionReturn
WrapRowProbeHeapReturn => OwnershipAtFunctionReturn
WrapRowUseSiteVerdictReturn => OwnershipAtFunctionReturn
WrapRowDiagnosticsParam => OwnershipAtFunctionParameter
WrapRowNodeParam => OwnershipAtFunctionParameter
WrapRowUseSiteVerdictParam => OwnershipAtFunctionParameter
WrapRowNodeStructField => OwnershipAtStructField
WrapRowDiagnosticsBinding => OwnershipAtBindingProjection
WrapRowNodeBinding => OwnershipAtBindingProjection
WrapRowTestClaimBinding => OwnershipAtBindingProjection
WrapRowFreeMonoidBinding => OwnershipAtBindingProjection
WrapRowOutcomeBinding => OwnershipAtBindingProjection
WrapRowModelCoreBinding => OwnershipAtBindingProjection
WrapRowAlgebraInhabitanceBinding => OwnershipAtBindingProjection
WrapRowProbeHeapBinding => OwnershipAtBindingProjection
WrapRowUseSiteVerdictBinding => OwnershipAtBindingProjection
}
}

fn rust_sg_rc_wrap_catalog_row_source_projection(key: OwnershipWrapCatalogRowKey) -> OwnershipWrapSourceProjection {
match key {
WrapRowTestClaimReturn => UseSiteOwnershipInstantiationHeadCarrier
WrapRowTestClaimBinding => UseSiteOwnershipInstantiationHeadCarrier
WrapRowOutcomeReturn => UseSiteOwnershipInstantiationHeadCarrier
WrapRowOutcomeBinding => UseSiteOwnershipInstantiationHeadCarrier
_ => UseSiteOwnershipExactCarrier
}
}

fn rust_sg_rc_wrap_catalog_row_reference_layer(key: OwnershipWrapCatalogRowKey) -> OwnershipReferenceLayer {
match key {
WrapRowDiagnosticsReturn => ReferenceLayerRc
WrapRowDiagnosticsParam => ReferenceLayerOwned
WrapRowDiagnosticsBinding => ReferenceLayerRc
WrapRowNodeReturn => ReferenceLayerRc
WrapRowNodeParam => ReferenceLayerOwned
WrapRowNodeStructField => ReferenceLayerBox
WrapRowNodeBinding => ReferenceLayerRc
WrapRowTestClaimReturn => ReferenceLayerRc
WrapRowTestClaimBinding => ReferenceLayerRc
WrapRowFreeMonoidReturn => ReferenceLayerRc
WrapRowFreeMonoidBinding => ReferenceLayerRc
WrapRowOutcomeReturn => ReferenceLayerRc
WrapRowOutcomeBinding => ReferenceLayerRc
WrapRowModelCoreReturn => ReferenceLayerRc
WrapRowModelCoreBinding => ReferenceLayerRc
WrapRowAlgebraInhabitanceReturn => ReferenceLayerRc
WrapRowAlgebraInhabitanceBinding => ReferenceLayerRc
WrapRowProbeHeapReturn => ReferenceLayerRc
WrapRowProbeHeapBinding => ReferenceLayerRc
WrapRowUseSiteVerdictReturn => ReferenceLayerOwned
WrapRowUseSiteVerdictParam => ReferenceLayerOwned
WrapRowUseSiteVerdictBinding => ReferenceLayerOwned
}
}

fn rust_sg_rc_wrap_carrier_key(type_name: String) -> String {
if type_name == "NonEmptyDiagnostics" {
"Diagnostics"
} else {
type_name
}
}

fn rust_sg_rc_wrap_carrier_from_type_name(type_name: String) -> OwnershipWrapCarrier? {
match rust_sg_rc_wrap_carrier_key(type_name: type_name) {
"Diagnostics" => Present { value: WrapCarrierDiagnostics }
"Node" => Present { value: WrapCarrierNode }
"TestClaim" => Present { value: WrapCarrierTestClaim }
"FreeMonoid" => Present { value: WrapCarrierFreeMonoid }
"Outcome" => Present { value: WrapCarrierOutcome }
"ModelCore" => Present { value: WrapCarrierModelCore }
"AlgebraInhabitanceDecl" => Present { value: WrapCarrierAlgebraInhabitanceDecl }
"ProbeHeap" => Present { value: WrapCarrierProbeHeap }
"UseSiteVerdict" => Present { value: WrapCarrierUseSiteVerdict }
_ => none
}
}

fn rust_sg_rc_ownership_wrap_catalog_rows() -> List<OwnershipWrapCatalogRowKey> {
[
WrapRowDiagnosticsReturn,
WrapRowDiagnosticsParam,
WrapRowDiagnosticsBinding,
WrapRowNodeReturn,
WrapRowNodeParam,
WrapRowNodeStructField,
WrapRowNodeBinding,
WrapRowTestClaimReturn,
WrapRowTestClaimBinding,
WrapRowFreeMonoidReturn,
WrapRowFreeMonoidBinding,
WrapRowOutcomeReturn,
WrapRowOutcomeBinding,
WrapRowModelCoreReturn,
WrapRowModelCoreBinding,
WrapRowAlgebraInhabitanceReturn,
WrapRowAlgebraInhabitanceBinding,
WrapRowProbeHeapReturn,
WrapRowProbeHeapBinding,
WrapRowUseSiteVerdictReturn,
WrapRowUseSiteVerdictParam,
WrapRowUseSiteVerdictBinding
]
}

fn rust_sg_rc_wrap_row_lookup_for_carrier(carrier: OwnershipWrapCarrier, use_site: OwnershipWrapUseSite) -> OwnershipReferenceLayer? {
rust_sg_rc_ownership_wrap_catalog_rows()
|> fold(
init: none,
f: (acc, key) =>
match acc {
Present { value: _ } => acc
Absent =>
if rust_sg_rc_wrap_catalog_row_carrier(key: key) == carrier && rust_sg_rc_wrap_catalog_row_use_site(key: key) == use_site {
Present { value: rust_sg_rc_wrap_catalog_row_reference_layer(key: key) }
} else {
acc
}
}
)
}

fn rust_sg_rc_carrier_enrolled_but_row_missing(type_name: String, use_site: OwnershipWrapUseSite) -> Bool {
match use_site {
OwnershipWrapUseSiteAbsent => false
_ =>
match rust_sg_rc_wrap_carrier_from_type_name(type_name: type_name) {
Present { value: carrier } =>
match rust_sg_rc_wrap_row_lookup_for_carrier(carrier: carrier, use_site: use_site) {
Present { value: _ } => false
Absent => true
}
Absent => false
}
}
}

fn rust_sg_rc_wrap_layer_lookup(type_name: String, use_site: OwnershipWrapUseSite) -> OwnershipReferenceLayer? {
match use_site {
OwnershipWrapUseSiteAbsent => none
_ =>
match rust_sg_rc_wrap_carrier_from_type_name(type_name: type_name) {
Present { value: carrier } => rust_sg_rc_wrap_row_lookup_for_carrier(carrier: carrier, use_site: use_site)
Absent => none
}
}
}

fn rust_sg_rc_wrap_layer_lookup_witness_holds() -> Bool {
match rust_sg_rc_wrap_layer_lookup(type_name: "Node", use_site: OwnershipAtStructField) {
Present { value: ReferenceLayerBox } =>
match rust_sg_rc_wrap_layer_lookup(type_name: "Node", use_site: OwnershipAtBindingProjection) {
Present { value: ReferenceLayerRc } => true
_ => false
}
_ => false
}
}

fn rust_sg_rc_carrier_enrolled_but_row_missing_witness_holds() -> Bool {
rust_sg_rc_carrier_enrolled_but_row_missing(type_name: "ProbeHeap", use_site: OwnershipAtFunctionParameter)
}
1 change: 1 addition & 0 deletions dag/gunbc/stage0_emit_model.dag
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ data generated_stage0_files: List<String> = [
"extdeps_languages_rust_emit.rs",
"extdeps_languages_rust_syntax.rs",
"extdeps_languages_rust_types.rs",
"extdeps_languages_rust_wrap_catalog.rs",
"extdeps_uri.rs",
"extdeps_uri_path.rs",
"extdeps_units_dimensionless.rs",
Expand Down
Loading