Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
46 commits
Select commit Hold shift + click to select a range
d11e768
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
25812e4
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
bf3a3f2
Merge remote-tracking branch 'origin/main' into session/nimble-dove-181
briansrls May 15, 2026
ee6e454
Merge remote-tracking branch 'origin/main' into session/nimble-dove-181
briansrls May 15, 2026
0bce650
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
e7de984
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
2920ffb
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
ade5b7f
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
b131afe
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
710e059
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
77158b7
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
d666844
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
e061d2a
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
a4dc9c6
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
7e9bd8a
chore(cost lens): tighten lens_cost_symbolic rustdoc before gate #104…
briansrls May 15, 2026
5322ded
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
69dede9
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
79d981d
chore: apply rustfmt to lens_cost_symbolic symbolic_cost_of (fixes CI…
briansrls May 15, 2026
f2a0b78
fix(cost lens): BindCycle Violates anchors at resolver detected_at node
briansrls May 15, 2026
b68a01b
Merge remote-tracking branch 'origin/main' into session/nimble-dove-181
briansrls May 15, 2026
b871d65
Merge remote-tracking branch 'origin/main' into session/nimble-dove-181
briansrls May 15, 2026
6d6bcaa
docs(cost): clarify dual lens read contracts (gate #104)
briansrls May 15, 2026
120c78c
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
6c40146
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
d539052
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
3b4c1c5
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
05f6b45
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
a63b801
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
12d5fae
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
0fe5041
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
8ce8481
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
8e68a30
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
61ee85c
Merge remote-tracking branch 'origin/main' into session/nimble-dove-181
briansrls May 15, 2026
ee77a79
docs(dimension): classify ViolatesSubject TERMINAL per Practice 4
briansrls May 15, 2026
bac0c01
Merge remote-tracking branch 'origin/main' into session/nimble-dove-181
briansrls May 15, 2026
cda5de4
docs(lens_cost_symbolic): align module rustdoc with ViolatesSubject v…
briansrls May 15, 2026
acf0291
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
deaa49c
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
8d2a267
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
1830219
feat(v3): ground ProducerLookup violates diagnostic spans via query port
briansrls May 15, 2026
5b1c973
Merge remote-tracking branch 'origin/main' into session/nimble-dove-181
briansrls May 15, 2026
6f4d3b0
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
f0158a7
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
644d9a8
WIP: Gate #104 lens_read_witness_shape_dissolved is DECLARED-status w…
briansrls May 15, 2026
b86430c
chore(bootstrap): resync snapshots for regen_bootstrap --verify
briansrls May 15, 2026
1bd80ff
docs(emit): note ViolatesSubject::AtBehavior tuple bridge parallels L…
briansrls May 15, 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
2 changes: 1 addition & 1 deletion docs/r3-program-plan.md

Large diffs are not rendered by default.

13,703 changes: 7,016 additions & 6,687 deletions src/v3/compiler/src/bootstrap_generated.rs

Large diffs are not rendered by default.

10,891 changes: 5,610 additions & 5,281 deletions src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion src/v3/compiler/src/complexity_lens_generated.rs
Original file line number Diff line number Diff line change
Expand Up @@ -580,7 +580,7 @@ pub fn witness_from_complexity_lookup(
reason: String::from(
"complexity_of: missing ComplexitySummary for behavior result port",
),
at: (p1).clone(),
subject: ViolatesSubject::AtBehavior((p1).clone()),
},
}
}
Expand Down
7 changes: 2 additions & 5 deletions src/v3/compiler/src/cost_symbolic_lens_generated.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,6 @@ pub struct SymbolicCostEntry {
pub port: PortId,
pub cost: Lookup<SymbolicCost>,
}
pub fn symbolic_cost_of(p0: &Dag, p1: &PortId) -> Lookup<SymbolicCost> {
lookup_cost(&(compute_symbolic_costs(p0)), p1)
}
pub fn method_contract_cost_shape(p0: &MethodContract) -> Option<CostShape> {
((p0).cost_shape).clone()
}
Expand Down Expand Up @@ -363,13 +360,13 @@ pub fn witness_from_symbolic_cost_lookup(
Lookup::Hit(c) => Witness::Inhabits((c).clone()),
Lookup::Miss => Witness::Violates {
reason: String::from("symbolic_cost_of: missing SymbolicCost for behavior result port"),
at: (p1).clone(),
subject: ViolatesSubject::AtBehavior((p1).clone()),
},
}
}
pub fn cost_lens_read(p0: &Dag, p1: Behavior) -> Witness<SymbolicCost> {
witness_from_symbolic_cost_lookup(
&(symbolic_cost_of(p0, &(behavior_result_port(&p1)))),
&(lookup_cost(&(compute_symbolic_costs(p0)), &(behavior_result_port(&p1)))),
(p1).clone(),
)
}
Expand Down
133 changes: 129 additions & 4 deletions src/v3/compiler/src/dimension.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,11 +41,74 @@ fn behavior_span(at: &Behavior) -> SourceSpan {
}
}

fn diagnostic_anchor_from_symbolic_cost_query_port(
d: &Dag,
query_port: &PortId,
) -> Option<SourceSpan> {
let port_ref = d.port_opt(query_port)?;
let producer = port_ref.produced_by?;
d.node_opt(&producer).map(behavior_span)
}

/// Hint for malformed-producer lookups when emitting [`Diagnostic`] rows from witnesses that only carry
/// [`ViolatesSubject::AtBehavior`] today: the offending behavior's own result [`PortId`] keyed the cost table
/// miss. [`ProducerLookupMissing*`](ViolatesSubject) witnesses have no authoritative query port baked into
/// the substrate residue — callers of [`violates_subject_diagnostic_span`] must pass **`Some(port)`** from
/// the same keyed query as [`lens_cost_symbolic::symbolic_cost_of`](crate::lens_cost_symbolic::symbolic_cost_of).
fn producer_lookup_anchor_hint(subject: &ViolatesSubject) -> Option<PortId> {
match subject {
ViolatesSubject::AtBehavior(b) => Some(behavior_result_port(b)),
ViolatesSubject::ProducerLookupMissingPort { .. }
| ViolatesSubject::ProducerLookupMissingNode { .. } => None,
}
}

/// IDE-/diagnostic-facing span for [`Witness::Violates`] when reporting
/// [`ViolatesSubject::ProducerLookupMissingPort`] /
/// [`ViolatesSubject::ProducerLookupMissingNode`].
///
/// Substrate residues name only offending [`PortId`] / [`NodeId`] handles —
/// carrying no source location. [`lens_cost_symbolic::symbolic_cost_of`](crate::lens_cost_symbolic::symbolic_cost_of)
/// is **port-keyed**; pass the **same `port`** it was called with here so diagnostics can anchor at the
/// consumer port's declaring [`Behavior`] (parity with [`ViolatesSubject::AtBehavior`]), instead of the
/// placeholder `malformed_substrate_producer_walk` sentinel used when **`lookup_port`** is unavailable.
///
/// [`ViolatesSubject::AtBehavior`]: ignores **`lookup_port`** and always attributes the offending behavior span.
#[must_use]
pub fn violates_subject_diagnostic_span(
d: &Dag,
lookup_port: Option<&PortId>,
subject: &ViolatesSubject,
) -> SourceSpan {
match subject {
ViolatesSubject::AtBehavior(b) => behavior_span(b),
ViolatesSubject::ProducerLookupMissingPort { .. }
| ViolatesSubject::ProducerLookupMissingNode { .. } => lookup_port
.and_then(|p| diagnostic_anchor_from_symbolic_cost_query_port(d, p))
.unwrap_or_else(|| SourceSpan::new("malformed_substrate_producer_walk", 0, 0)),
}
}

/// Evidence partition — mirrors `Witness<Carrier>` in `std/dimensions.dag`.
#[derive(Debug, Clone)]
pub enum Witness<C> {
Inhabits(C),
Violates { reason: String, at: Behavior },
Violates {
reason: String,
subject: ViolatesSubject,
},
}

/// 🟢 TERMINAL coproduct (**Practice 4** / `docs/modeling-discipline.md` §4):
/// hand mirror of `ViolatesSubject` in `src/v3/std/dimensions.dag`. Variants are the discriminated outcomes
/// of the producer walk ([`crate::dag::ProducerLookup`]) paired with lawful `Behavior` attribution — not a
/// decomposable record without collapsing P3 fail-closed residue. **Ledger:** dissolution patterns 1–4 in §4
/// do not apply; substrate + `Witness::Violates.subject` already name the single authority (gate #104).
#[derive(Debug, Clone)]
pub enum ViolatesSubject {
AtBehavior(Behavior),
ProducerLookupMissingPort { port: PortId },
ProducerLookupMissingNode { producer: NodeId },
}

/// Report carrier — mirrors `DimensionReport<Carrier>` in `std/dimensions.dag`.
Expand Down Expand Up @@ -171,7 +234,7 @@ pub fn analyze_symbolic_cost_dimension(
match lookup_symbolic_cost(&cost_table, &port) {
SymbolicCostLookup::Miss => witnesses.push(Witness::Violates {
reason: "missing symbolic cost for behavior result port".into(),
at: behavior.clone(),
subject: ViolatesSubject::AtBehavior(behavior.clone()),
}),
SymbolicCostLookup::Hit(cost) => witnesses.push(Witness::Inhabits(cost)),
}
Expand All @@ -197,12 +260,16 @@ pub fn analyze_symbolic_cost_dimension(
let mut violations: Vec<Diagnostic> = witnesses
.iter()
.filter_map(|w| {
let Witness::Violates { reason, at } = w else {
let Witness::Violates { reason, subject } = w else {
return None;
};
Some(Diagnostic::ParseError {
message: format!("symbolic_cost dimension: {reason}"),
span: behavior_span(at),
span: violates_subject_diagnostic_span(
d,
producer_lookup_anchor_hint(subject).as_ref(),
subject,
),
correction: Correction::deferred_for_diagnostic_class(
"SymbolicCostDimensionDiagnostic",
),
Expand Down Expand Up @@ -540,3 +607,61 @@ mod fail_closed_tests {
);
}
}

#[cfg(test)]
mod violates_subject_diagnostic_span_tests {
use super::*;
use crate::dag::{literal_bits_int, Dag, PortId};

#[test]
fn producer_lookup_residue_prefers_consumer_behavior_span_when_keyed_port_given() {
let mut dag = Dag::new();
let anchored = SourceSpan::new("fixture_cost_port.dag", 11, 19);
let value_out = dag.push_value(literal_bits_int(42), anchored.clone());
let subject = ViolatesSubject::ProducerLookupMissingPort {
port: PortId::test_raw(999),
};

assert_eq!(
violates_subject_diagnostic_span(&dag, Some(&value_out), &subject),
anchored
);
assert_eq!(
violates_subject_diagnostic_span(&dag, None, &subject),
SourceSpan::new("malformed_substrate_producer_walk", 0, 0),
);

let node_miss = ViolatesSubject::ProducerLookupMissingNode {
producer: crate::dag::NodeId::from_table_index(424242),
};
assert_eq!(
violates_subject_diagnostic_span(&dag, Some(&value_out), &node_miss),
anchored
);
}

#[test]
fn at_behavior_always_anchors_the_subject_even_if_lookup_hint_differs() {
let mut dag = Dag::new();
let s1 = SourceSpan::new("subject_behavior.dag", 1, 4);
let s2 = SourceSpan::new("other_port_noise.dag", 77, 88);
let p_subj = dag.push_value(literal_bits_int(11), s1.clone());
let p_other = dag.push_value(literal_bits_int(22), s2.clone());
let nid = dag
.port_opt(&p_subj)
.expect("literal port wired")
.produced_by
.expect("value node should produce output port");
let b_subj = dag.node(nid).clone();

assert_eq!(
violates_subject_diagnostic_span(
&dag,
Some(&p_other),
&ViolatesSubject::AtBehavior(b_subj),
),
s1,
"hint must not override declared subject behavior attribution",
);
}
}
36 changes: 36 additions & 0 deletions src/v3/compiler/src/emit/rust_target.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4304,6 +4304,21 @@ impl<'a> Ctx<'a> {
&[("name", qualified_name), ("binding", rendered_binding)],
));
}
// `ViolatesSubject::AtBehavior` is a Rust tuple variant (gate #104 / `dimensions.dag`
// mirrors `ViolatesSubject`); without this arm, emit renders named-field `_0:` patterns for
// the single-payload disj stub. Same dissolution trigger as `Lookup`/`Hit` above: positional
// vs struct payloads are not modeled structurally on the Disj emission surface yet.
let is_violates_subject_at_behavior = field_name == "_0"
&& matches!(
qualified_name.split("::").collect::<Vec<_>>().as_slice(),
[a, b] if *a == "ViolatesSubject" && *b == "AtBehavior"
);
if is_violates_subject_at_behavior {
return Some(render_named_template(
&self.indexes.syntax.patterns.variant_pattern_positional,
&[("name", qualified_name), ("binding", rendered_binding)],
));
}
let bindings = render_named_template(
&self.indexes.syntax.patterns.field_binding,
&[("field", field_name), ("binding", rendered_binding)],
Expand Down Expand Up @@ -4940,6 +4955,7 @@ impl<'a> Ctx<'a> {
// Dissolution: same "tuple `Hit` for `v3.std.lookup` only" bridge as
// `render_single_field_variant_pattern` (pattern side); see long comment
// there. Until variant payload positionality is DAG-carried, keep narrow.
// `ViolatesSubject::AtBehavior` tuple emission matches `dimension.rs`.
if children.len() == 1
&& children[0].label == "_0"
&& enum_name == "Witness"
Expand Down Expand Up @@ -4978,6 +4994,26 @@ impl<'a> Ctx<'a> {
};
return Ok(Some(out));
}
// `ViolatesSubject::AtBehavior(Behavior)` is a Rust **tuple** variant in
// `dimension.rs` (`std/dimensions.dag` unary payload). Default emit would render
// `{ _0: … }` struct init and fail against the hand mirror tuple shape.
if children.len() == 1
&& children[0].label == "_0"
&& enum_name == "ViolatesSubject"
&& variant_name == "AtBehavior"
{
let value = self.elide_explicit_borrow(&self.render_input_use(
InputConsumer::Transform(consumer),
InputSlot::Positional(0),
locals,
)?);
let payload = if value.contains(".clone()") {
value
} else {
format!("({value}).clone()")
};
return Ok(Some(format!("{qualified_name}({payload})")));
}
let fields = children
.iter()
.enumerate()
Expand Down
Loading
Loading