From af2bcf39f9f49388186511f45531847779497d30 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 1 May 2026 06:02:10 -0400 Subject: [PATCH 1/3] WIP: R3 Substrate --- .../integration/bridge_ledger_carrier_test.rs | 13 +++++---- src/v3/std/bridge_ledger.dag | 27 ++++++++++++++----- 2 files changed, 26 insertions(+), 14 deletions(-) diff --git a/src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs b/src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs index b9677809386..f66df2838d5 100644 --- a/src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs +++ b/src/v3/compiler/tests/integration/bridge_ledger_carrier_test.rs @@ -259,13 +259,12 @@ fn bridge_ledger_zero_predicate_carries_only_ledger_bridge_ledger_ref() { #[test] fn bridge_ledger_zero_runner_fails_with_named_open_rows_at_head() { - // At HEAD the canonical ledger has three Open rows - // (source_span_file_participation, include_str_side_channels, - // exact_string_patching_residual). The runner must `Fail` and name - // every Open row in the diagnostic; do NOT pretend ledger-zero is - // already true. Once an `Open` row flips to `Retired` upstream the - // diagnostic narrows to the remaining open names; once all five are - // `Retired` this test re-arms as a `Pass` ratchet. + // At HEAD the canonical ledger still has Open rows. The runner must + // `Fail` and name every Open row in the diagnostic; do NOT pretend + // ledger-zero is already true. Once an `Open` row flips to + // `Retired` upstream the diagnostic narrows to the remaining open + // names; once all rows are `Retired` this test re-arms as a `Pass` + // ratchet. let source = r#" data ledger_zero_claim: TestClaim = { name: "bridge_ledger_zero_at_head", diff --git a/src/v3/std/bridge_ledger.dag b/src/v3/std/bridge_ledger.dag index 690eeb80088..a99d2b74805 100644 --- a/src/v3/std/bridge_ledger.dag +++ b/src/v3/std/bridge_ledger.dag @@ -40,10 +40,15 @@ import v3.spec.v3_l1 { DeclarationRef } // Per `r3-structure.md:80`: "name-keyed bootstrap bridge from #937 // deleted; nominal-opacity authority lives in source-level // declaration (PR A landed in R2)." -// - `bridge_canonical_lens_name_dispatch_retired` — Retired. Lens -// dispatch routes via `DeclarationRef`/typed identity; ratcheted by -// `canonical_lens_bridge_ratchet_test.rs` (R2 PB canonical-lens -// bridge ratchet, PR #1183 disposition). +// - `bridge_canonical_lens_name_dispatch_pr1183_slice_retired` — +// Retired. Narrow PR #1183 slice: lens dispatch routes via +// `DeclarationRef`/typed identity; ratcheted by +// `canonical_lens_bridge_ratchet_test.rs`. +// - `bridge_canonical_lens_name_patching_residual` — Open. Broader +// exact-string canonical-lens-name class remains live in +// `test_runner.rs` (`include_str!`, name arms, and generic +// name-keyed lookups); full retirement waits for PB-Runtime +// interpreter-as-data or a typed lens-registry carrier. // - `bridge_include_str_side_channels_retired` — Open. Per // `r3-structure.md:82`: "Open disposition (`pipeline_authority`, // PR #1171, 2026-04-29): `compile` remains `ArrowBody::Unparsed`, @@ -107,8 +112,10 @@ type BridgeLedgerRow { authority: String } -// Five canonical bridge-retirement rows. Authoring order matches -// `docs/r3-structure.md:79-83`. Per-row `authority` points at the +// Canonical bridge-retirement rows. Authoring order follows +// `docs/r3-structure.md:79-83`; split rows enumerate sub-classes when +// one prose bridge has both a retired slice and a remaining residual. +// Per-row `authority` points at the // concrete ratchet (test, PR, gating doc-anchor) that establishes // the row's status — not a generic taxonomy heading. Status flips // from `Open` to `Retired` are gated on the named ratchet reaching @@ -127,11 +134,17 @@ data bridge_ledger: List = [ authority: "PR #937" }, { - name: "bridge_canonical_lens_name_dispatch_retired", + name: "bridge_canonical_lens_name_dispatch_pr1183_slice_retired", owner: "R2-Substrate", status: Retired, authority: "src/v3/compiler/tests/integration/canonical_lens_bridge_ratchet_test.rs" }, + { + name: "bridge_canonical_lens_name_patching_residual", + owner: "PB-Runtime", + status: Open, + authority: "docs/briefs/r2-pb-canonical-lens-bridge-disposition.md" + }, { name: "bridge_include_str_side_channels_retired", owner: "pipeline_authority", From 426753309a1d54056e11ea08de7a5b0e81d4651e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 1 May 2026 06:06:41 -0400 Subject: [PATCH 2/3] WIP: R3 Substrate --- src/v3/compiler/src/bootstrap_generated.rs | 14 +++++++------- .../bootstrap_generated_without_parse_surface.rs | 14 +++++++------- .../tests/integration/parse_corpus_manifest.txt | 2 +- 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/v3/compiler/src/bootstrap_generated.rs b/src/v3/compiler/src/bootstrap_generated.rs index 6946cfd032a..4440b7e90c6 100644 --- a/src/v3/compiler/src/bootstrap_generated.rs +++ b/src/v3/compiler/src/bootstrap_generated.rs @@ -795,10 +795,10 @@ pub(crate) fn bootstrapped_fixture_dag() -> Dag { Declaration { id: DeclarationId(787), name: Some("AnthropicMessages200Usage".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "input_tokens".to_string(), ty: DeclarationId(74) }, Field { label: "output_tokens".to_string(), ty: DeclarationId(74) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/anthropic_schema.dag", 4994, 5070) }, Declaration { id: DeclarationId(788), name: Some("AnthropicMessages200Body".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "id".to_string(), ty: DeclarationId(189) }, Field { label: "type".to_string(), ty: DeclarationId(189) }, Field { label: "role".to_string(), ty: DeclarationId(189) }, Field { label: "content".to_string(), ty: DeclarationId(1722) }, Field { label: "model".to_string(), ty: DeclarationId(189) }, Field { label: "stop_reason".to_string(), ty: DeclarationId(785) }, Field { label: "stop_sequence".to_string(), ty: DeclarationId(1723) }, Field { label: "usage".to_string(), ty: DeclarationId(787) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/anthropic_schema.dag", 5417, 5704) }, Declaration { id: DeclarationId(789), name: Some("BinShim".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "entrypoint_name".to_string(), ty: DeclarationId(114) }, Field { label: "description".to_string(), ty: DeclarationId(189) }, Field { label: "entry".to_string(), ty: DeclarationId(1049) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bin_shim.dag", 801, 894) }, - Declaration { id: DeclarationId(790), name: Some("BridgeStatus".to_string()), connective: TypeConnective::Disj { variants: vec![Field { label: "Retired".to_string(), ty: DeclarationId(1724) }, Field { label: "Open".to_string(), ty: DeclarationId(1725) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 3992, 4030) }, - Declaration { id: DeclarationId(791), name: Some("BridgeLedgerRef".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "decl".to_string(), ty: DeclarationId(1049) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4994, 5041) }, - Declaration { id: DeclarationId(792), name: Some("BridgeLedgerRow".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "name".to_string(), ty: DeclarationId(189) }, Field { label: "owner".to_string(), ty: DeclarationId(189) }, Field { label: "status".to_string(), ty: DeclarationId(790) }, Field { label: "authority".to_string(), ty: DeclarationId(189) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 5684, 5794) }, - Declaration { id: DeclarationId(793), name: Some("bridge_ledger".to_string()), connective: TypeConnective::Instantiation { template: DeclarationId(592), arguments: vec![TemplateArgument { parameter: DeclarationId(593), value: DeclarationId(792) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: Some(DeclarationId(1726)), specialization_parent: None, inhabits: None, value_body: Some(ValueBody::List(vec![FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_source_span_file_participation_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R3".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1725), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("ROADMAP.md#lens-fold-file-path-semantics".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_mark_bootstrap_secret_nominal_opacity_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R2-Substrate".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1724), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("PR #937".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_canonical_lens_name_dispatch_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R2-Substrate".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1724), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("src/v3/compiler/tests/integration/canonical_lens_bridge_ratchet_test.rs".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_include_str_side_channels_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("pipeline_authority".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1725), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("PR #1171".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_exact_string_patching_residual_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("PB-Tier-2".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1725), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("docs/r3-structure.md:83".to_string())))])])), refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6151, 7701) }, + Declaration { id: DeclarationId(790), name: Some("BridgeStatus".to_string()), connective: TypeConnective::Disj { variants: vec![Field { label: "Retired".to_string(), ty: DeclarationId(1724) }, Field { label: "Open".to_string(), ty: DeclarationId(1725) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4292, 4330) }, + Declaration { id: DeclarationId(791), name: Some("BridgeLedgerRef".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "decl".to_string(), ty: DeclarationId(1049) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 5294, 5341) }, + Declaration { id: DeclarationId(792), name: Some("BridgeLedgerRow".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "name".to_string(), ty: DeclarationId(189) }, Field { label: "owner".to_string(), ty: DeclarationId(189) }, Field { label: "status".to_string(), ty: DeclarationId(790) }, Field { label: "authority".to_string(), ty: DeclarationId(189) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 5984, 6094) }, + Declaration { id: DeclarationId(793), name: Some("bridge_ledger".to_string()), connective: TypeConnective::Instantiation { template: DeclarationId(592), arguments: vec![TemplateArgument { parameter: DeclarationId(593), value: DeclarationId(792) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: Some(DeclarationId(1726)), specialization_parent: None, inhabits: None, value_body: Some(ValueBody::List(vec![FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_source_span_file_participation_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R3".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1725), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("ROADMAP.md#lens-fold-file-path-semantics".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_mark_bootstrap_secret_nominal_opacity_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R2-Substrate".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1724), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("PR #937".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_canonical_lens_name_dispatch_pr1183_slice_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R2-Substrate".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1724), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("src/v3/compiler/tests/integration/canonical_lens_bridge_ratchet_test.rs".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_canonical_lens_name_patching_residual".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("PB-Runtime".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1725), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("docs/briefs/r2-pb-canonical-lens-bridge-disposition.md".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_include_str_side_channels_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("pipeline_authority".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1725), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("PR #1171".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_exact_string_patching_residual_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("PB-Tier-2".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1725), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("docs/r3-structure.md:83".to_string())))])])), refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6558, 8315) }, Declaration { id: DeclarationId(794), name: Some("CleanEmissionContract".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "expression_wrapping".to_string(), ty: DeclarationId(796) }, Field { label: "pattern_bindings".to_string(), ty: DeclarationId(797) }, Field { label: "variant_payload_field_access".to_string(), ty: DeclarationId(798) }, Field { label: "imports".to_string(), ty: DeclarationId(799) }, Field { label: "block_return".to_string(), ty: DeclarationId(800) }, Field { label: "variable_bindings".to_string(), ty: DeclarationId(801) }, Field { label: "match_arm_body".to_string(), ty: DeclarationId(802) }, Field { label: "correction_style".to_string(), ty: DeclarationId(803) }, Field { label: "post_emit_verifier".to_string(), ty: DeclarationId(804) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/clean_emission.dag", 562, 944) }, Declaration { id: DeclarationId(795), name: Some("TargetCleanEmissionBinding".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "language".to_string(), ty: DeclarationId(898) }, Field { label: "clean_emission".to_string(), ty: DeclarationId(794) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/clean_emission.dag", 1748, 1848) }, Declaration { id: DeclarationId(796), name: Some("ExpressionWrappingRule".to_string()), connective: TypeConnective::Disj { variants: vec![Field { label: "WrapEverything".to_string(), ty: DeclarationId(1727) }, Field { label: "WrapOnlyInOperandPosition".to_string(), ty: DeclarationId(1728) }, Field { label: "NoWrapping".to_string(), ty: DeclarationId(1729) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/clean_emission.dag", 2192, 2283) }, @@ -1729,9 +1729,9 @@ pub(crate) fn bootstrapped_fixture_dag() -> Dag { Declaration { id: DeclarationId(1721), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/anthropic_schema.dag", 4178, 4204) }, Declaration { id: DeclarationId(1722), name: None, connective: TypeConnective::Instantiation { template: DeclarationId(592), arguments: vec![TemplateArgument { parameter: DeclarationId(593), value: DeclarationId(786) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/anthropic_schema.dag", 5538, 5573) }, Declaration { id: DeclarationId(1723), name: None, connective: TypeConnective::Cardinality(CardinalityPayload::new_unchecked(DeclarationId(189), CardinalityBound::AtMostOne)), type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/anthropic_schema.dag", 5652, 5659) }, - Declaration { id: DeclarationId(1724), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4014, 4021) }, - Declaration { id: DeclarationId(1725), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4026, 4030) }, - Declaration { id: DeclarationId(1726), name: None, connective: TypeConnective::Instantiation { template: DeclarationId(592), arguments: vec![TemplateArgument { parameter: DeclarationId(593), value: DeclarationId(792) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6171, 6192) }, + Declaration { id: DeclarationId(1724), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4314, 4321) }, + Declaration { id: DeclarationId(1725), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4326, 4330) }, + Declaration { id: DeclarationId(1726), name: None, connective: TypeConnective::Instantiation { template: DeclarationId(592), arguments: vec![TemplateArgument { parameter: DeclarationId(593), value: DeclarationId(792) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6578, 6599) }, Declaration { id: DeclarationId(1727), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/clean_emission.dag", 2224, 2238) }, Declaration { id: DeclarationId(1728), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/clean_emission.dag", 2243, 2268) }, Declaration { id: DeclarationId(1729), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/clean_emission.dag", 2273, 2283) }, diff --git a/src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs b/src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs index f1beca52a63..ef0f3d67e47 100644 --- a/src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs +++ b/src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs @@ -795,10 +795,10 @@ pub(crate) fn bootstrapped_fixture_without_parse_surface_dag() -> Dag { Declaration { id: DeclarationId(787), name: Some("AnthropicMessages200Usage".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "input_tokens".to_string(), ty: DeclarationId(74) }, Field { label: "output_tokens".to_string(), ty: DeclarationId(74) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/anthropic_schema.dag", 4994, 5070) }, Declaration { id: DeclarationId(788), name: Some("AnthropicMessages200Body".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "id".to_string(), ty: DeclarationId(189) }, Field { label: "type".to_string(), ty: DeclarationId(189) }, Field { label: "role".to_string(), ty: DeclarationId(189) }, Field { label: "content".to_string(), ty: DeclarationId(1707) }, Field { label: "model".to_string(), ty: DeclarationId(189) }, Field { label: "stop_reason".to_string(), ty: DeclarationId(785) }, Field { label: "stop_sequence".to_string(), ty: DeclarationId(1708) }, Field { label: "usage".to_string(), ty: DeclarationId(787) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/anthropic_schema.dag", 5417, 5704) }, Declaration { id: DeclarationId(789), name: Some("BinShim".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "entrypoint_name".to_string(), ty: DeclarationId(114) }, Field { label: "description".to_string(), ty: DeclarationId(189) }, Field { label: "entry".to_string(), ty: DeclarationId(1034) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bin_shim.dag", 801, 894) }, - Declaration { id: DeclarationId(790), name: Some("BridgeStatus".to_string()), connective: TypeConnective::Disj { variants: vec![Field { label: "Retired".to_string(), ty: DeclarationId(1709) }, Field { label: "Open".to_string(), ty: DeclarationId(1710) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 3992, 4030) }, - Declaration { id: DeclarationId(791), name: Some("BridgeLedgerRef".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "decl".to_string(), ty: DeclarationId(1034) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4994, 5041) }, - Declaration { id: DeclarationId(792), name: Some("BridgeLedgerRow".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "name".to_string(), ty: DeclarationId(189) }, Field { label: "owner".to_string(), ty: DeclarationId(189) }, Field { label: "status".to_string(), ty: DeclarationId(790) }, Field { label: "authority".to_string(), ty: DeclarationId(189) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 5684, 5794) }, - Declaration { id: DeclarationId(793), name: Some("bridge_ledger".to_string()), connective: TypeConnective::Instantiation { template: DeclarationId(592), arguments: vec![TemplateArgument { parameter: DeclarationId(593), value: DeclarationId(792) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: Some(DeclarationId(1711)), specialization_parent: None, inhabits: None, value_body: Some(ValueBody::List(vec![FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_source_span_file_participation_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R3".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1710), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("ROADMAP.md#lens-fold-file-path-semantics".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_mark_bootstrap_secret_nominal_opacity_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R2-Substrate".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1709), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("PR #937".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_canonical_lens_name_dispatch_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R2-Substrate".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1709), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("src/v3/compiler/tests/integration/canonical_lens_bridge_ratchet_test.rs".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_include_str_side_channels_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("pipeline_authority".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1710), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("PR #1171".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_exact_string_patching_residual_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("PB-Tier-2".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1710), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("docs/r3-structure.md:83".to_string())))])])), refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6151, 7701) }, + Declaration { id: DeclarationId(790), name: Some("BridgeStatus".to_string()), connective: TypeConnective::Disj { variants: vec![Field { label: "Retired".to_string(), ty: DeclarationId(1709) }, Field { label: "Open".to_string(), ty: DeclarationId(1710) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4292, 4330) }, + Declaration { id: DeclarationId(791), name: Some("BridgeLedgerRef".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "decl".to_string(), ty: DeclarationId(1034) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 5294, 5341) }, + Declaration { id: DeclarationId(792), name: Some("BridgeLedgerRow".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "name".to_string(), ty: DeclarationId(189) }, Field { label: "owner".to_string(), ty: DeclarationId(189) }, Field { label: "status".to_string(), ty: DeclarationId(790) }, Field { label: "authority".to_string(), ty: DeclarationId(189) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 5984, 6094) }, + Declaration { id: DeclarationId(793), name: Some("bridge_ledger".to_string()), connective: TypeConnective::Instantiation { template: DeclarationId(592), arguments: vec![TemplateArgument { parameter: DeclarationId(593), value: DeclarationId(792) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: Some(DeclarationId(1711)), specialization_parent: None, inhabits: None, value_body: Some(ValueBody::List(vec![FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_source_span_file_participation_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R3".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1710), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("ROADMAP.md#lens-fold-file-path-semantics".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_mark_bootstrap_secret_nominal_opacity_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R2-Substrate".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1709), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("PR #937".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_canonical_lens_name_dispatch_pr1183_slice_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("R2-Substrate".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1709), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("src/v3/compiler/tests/integration/canonical_lens_bridge_ratchet_test.rs".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_canonical_lens_name_patching_residual".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("PB-Runtime".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1710), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("docs/briefs/r2-pb-canonical-lens-bridge-disposition.md".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_include_str_side_channels_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("pipeline_authority".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1710), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("PR #1171".to_string())))]), FieldValue::Record(vec![("name".to_string(), FieldValue::Literal(LiteralBits::String("bridge_exact_string_patching_residual_retired".to_string()))), ("owner".to_string(), FieldValue::Literal(LiteralBits::String("PB-Tier-2".to_string()))), ("status".to_string(), FieldValue::Variant { constructor: DeclarationId(1710), payload: vec![] }), ("authority".to_string(), FieldValue::Literal(LiteralBits::String("docs/r3-structure.md:83".to_string())))])])), refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6558, 8315) }, Declaration { id: DeclarationId(794), name: Some("CleanEmissionContract".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "expression_wrapping".to_string(), ty: DeclarationId(796) }, Field { label: "pattern_bindings".to_string(), ty: DeclarationId(797) }, Field { label: "variant_payload_field_access".to_string(), ty: DeclarationId(798) }, Field { label: "imports".to_string(), ty: DeclarationId(799) }, Field { label: "block_return".to_string(), ty: DeclarationId(800) }, Field { label: "variable_bindings".to_string(), ty: DeclarationId(801) }, Field { label: "match_arm_body".to_string(), ty: DeclarationId(802) }, Field { label: "correction_style".to_string(), ty: DeclarationId(803) }, Field { label: "post_emit_verifier".to_string(), ty: DeclarationId(804) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/clean_emission.dag", 562, 944) }, Declaration { id: DeclarationId(795), name: Some("TargetCleanEmissionBinding".to_string()), connective: TypeConnective::Conj { children: vec![Field { label: "language".to_string(), ty: DeclarationId(898) }, Field { label: "clean_emission".to_string(), ty: DeclarationId(794) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/clean_emission.dag", 1748, 1848) }, Declaration { id: DeclarationId(796), name: Some("ExpressionWrappingRule".to_string()), connective: TypeConnective::Disj { variants: vec![Field { label: "WrapEverything".to_string(), ty: DeclarationId(1712) }, Field { label: "WrapOnlyInOperandPosition".to_string(), ty: DeclarationId(1713) }, Field { label: "NoWrapping".to_string(), ty: DeclarationId(1714) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/clean_emission.dag", 2192, 2283) }, @@ -1714,9 +1714,9 @@ pub(crate) fn bootstrapped_fixture_without_parse_surface_dag() -> Dag { Declaration { id: DeclarationId(1706), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/anthropic_schema.dag", 4178, 4204) }, Declaration { id: DeclarationId(1707), name: None, connective: TypeConnective::Instantiation { template: DeclarationId(592), arguments: vec![TemplateArgument { parameter: DeclarationId(593), value: DeclarationId(786) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/anthropic_schema.dag", 5538, 5573) }, Declaration { id: DeclarationId(1708), name: None, connective: TypeConnective::Cardinality(CardinalityPayload::new_unchecked(DeclarationId(189), CardinalityBound::AtMostOne)), type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/anthropic_schema.dag", 5652, 5659) }, - Declaration { id: DeclarationId(1709), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4014, 4021) }, - Declaration { id: DeclarationId(1710), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4026, 4030) }, - Declaration { id: DeclarationId(1711), name: None, connective: TypeConnective::Instantiation { template: DeclarationId(592), arguments: vec![TemplateArgument { parameter: DeclarationId(593), value: DeclarationId(792) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6171, 6192) }, + Declaration { id: DeclarationId(1709), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4314, 4321) }, + Declaration { id: DeclarationId(1710), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 4326, 4330) }, + Declaration { id: DeclarationId(1711), name: None, connective: TypeConnective::Instantiation { template: DeclarationId(592), arguments: vec![TemplateArgument { parameter: DeclarationId(593), value: DeclarationId(792) }] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/bridge_ledger.dag", 6578, 6599) }, Declaration { id: DeclarationId(1712), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/clean_emission.dag", 2224, 2238) }, Declaration { id: DeclarationId(1713), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/clean_emission.dag", 2243, 2268) }, Declaration { id: DeclarationId(1714), name: None, connective: TypeConnective::Conj { children: vec![] }, type_params: vec![], phantom_params: Vec::new(), meta_tag: None, specialization_parent: None, inhabits: None, value_body: None, refinement: None, nominal_opacity: None, span: SourceSpan::new("src/v3/std/clean_emission.dag", 2273, 2283) }, diff --git a/src/v3/compiler/tests/integration/parse_corpus_manifest.txt b/src/v3/compiler/tests/integration/parse_corpus_manifest.txt index 9fb7a3345a0..1b4a7642e53 100644 --- a/src/v3/compiler/tests/integration/parse_corpus_manifest.txt +++ b/src/v3/compiler/tests/integration/parse_corpus_manifest.txt @@ -27,7 +27,7 @@ src/v3/std/anthropic_messages.dag 5 6056 25140dcf6faa8e6b src/v3/std/anthropic_operations.dag 6 3404 a729e7662be9af5f src/v3/std/anthropic_schema.dag 8 20682 cdd44a074743988b src/v3/std/bin_shim.dag 4 2544 9ac96f1b3feafe47 -src/v3/std/bridge_ledger.dag 7 27382 fdcd9c26dc2b70b0 +src/v3/std/bridge_ledger.dag 7 31662 ec3b4ea8c0455eb7 src/v3/std/clean_emission.dag 15 23867 e7bc1e6145f4781e src/v3/std/computation.dag 18 36754 8023f388c3fb0918 src/v3/std/computation_model.dag 14 22953 20e458fe097d175a From 65adce81daf3cca94058fac8793c2eb8a35199eb Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 2 May 2026 19:55:39 -0400 Subject: [PATCH 3/3] fix(r3): correct SubValueRelation algebra claim --- src/v3/std/induction.dag | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/v3/std/induction.dag b/src/v3/std/induction.dag index 64cbcde97b8..5eee8706b7d 100644 --- a/src/v3/std/induction.dag +++ b/src/v3/std/induction.dag @@ -245,7 +245,7 @@ fn sub_value_to_evidence(relation: SubValueRelation) -> DescentEvidence { // ========================================================================= -// SubValueRelation lattice: meet/join for conservative/optimistic merge +// SubValueRelation merge helpers // ========================================================================= // Structural equality on shrink rates (P2 single authority for cost-relevant @@ -276,7 +276,8 @@ fn shrink_factor_eq(a: ShrinkFactor, b: ShrinkFactor) -> Bool { // (`shrink_factor_eq`); otherwise the merge is incomparable → SubValueUnknown. // Different fields/params remain incomparable as before. // -// Lattice ordering: SubValueUnknown < PreservedValue < {structural variants} +// This is a fail-closed meet-oriented helper, not a bounded-lattice witness: +// PreservedValue is a "same argument" relation, not a top element. fn meet_sub_value(a: SubValueRelation, b: SubValueRelation) -> SubValueRelation { match a { @@ -369,11 +370,11 @@ fn join_sub_value(a: SubValueRelation, b: SubValueRelation) -> SubValueRelation } } -// SubValueRelation inhabits BoundedLattice: -// meet = meet_sub_value, join = join_sub_value -// top = PreservedValue (meet identity), bottom = SubValueUnknown -// Data declaration deferred: compiler does not yet emit generic type -// parameters for data constants (BoundedLattice). +// SubValueRelation intentionally does not claim BoundedLattice inhabitance: +// meet_sub_value is the conservative fail-closed merge helper. +// join_sub_value is an optimistic auxiliary helper. +// SubValueUnknown is the fail-closed sink and join identity. +// PreservedValue is a same-argument relation, not a meet identity/top. // =========================================================================