Repository navigation
feat(v3): workflow_root_port accessor + WorkflowRoot sum (Prereq-3a) #1232
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from all commits
bd8725b
2fd9eed
7994d36
fd494f6
ef14405
57bbd40
d92b3e0
186c0f8
4602659
208150a
660e2ab
51fb2b4
6496a0c
7f475e0
2c13dc8
61ad6ea
b18a5ec
b7e6988
66fa643
45f24c9
0ef4771
fa5bba2
cdcaecc
c515b7e
818126b
5bb049c
1eeadb7
d1d2599
b0eb3d8
ec597ac
1f695fe
c865541
d6216b8
b9cf95f
fdaaee5
b2651ac
84755ce
7900975
ad39ecb
944cf79
073b077
b5359e2
b8d8693
9056936
359f658
83535ad
d34ca4a
8db65f7
a49a8aa
09c221e
42bf818
a4950f5
cca85a6
8f48849
ffd5723
96c9901
c00b862
f2f3128
b278ce0
b37da92
d4281ad
7cd7f06
4c72876
9f718b3
a3f6ac5
0304df1
8a9c259
b7f66fd
cd53fc5
ed8997c
1deb963
93c6f45
9aaee8e
5432a05
6000ecd
092b0c2
5e9a47f
55b2936
628910c
8bb6dc7
428c341
3d9569a
dc0b369
46e632c
4ed2a8e
d4d4e85
c135320
aa5da8c
0fbd045
6dae6c4
473d743
a35ff9d
ed361c4
b340837
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Large diffs are not rendered by default.
Large diffs are not rendered by default.
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -1906,6 +1906,41 @@ pub enum Behavior { | |
| Bind(BindNode), | ||
| } | ||
|
|
||
| /// Workflow-root identification — Rust mirror of | ||
| /// [`crate::dag::WorkflowRoot`]'s declaration in | ||
| /// `src/v3/std/substrate.dag`. | ||
| /// | ||
| /// 🟡 SCAFFOLD coproduct (mirroring the .dag receipt). The three arms | ||
| /// partition every legitimate `Dag` exactly once: | ||
| /// | ||
| /// - `SingleRoot(p)` — α (last topological `Bind`) selected `p`. | ||
| /// Emitted whenever the Dag contains at least one `Bind`; multiple | ||
| /// Binds are NOT ambiguous under α — linear `d.nodes` picks | ||
| /// exactly one last element by definition. | ||
| /// - `NoRoot` — zero `Bind` behaviors in `d.nodes`. Lens fold short- | ||
| /// circuits to `DimensionFail`; runtime evaluation rejects. | ||
| /// - `AmbiguousRoot { candidates }` — reserved for the future | ||
| /// enumerate-all-eligible-entries rule that R2-Evaluator's | ||
| /// `evaluate(program, entry, args)` consumes for multi-entry | ||
| /// programs (per Items 4+5 / #1176 §3.2). The α / γ "last X Bind" | ||
| /// rules cannot populate this arm; today's α implementation never | ||
| /// emits it. Carried as `NonSingletonList<PortId>` to make the | ||
| /// pre-disambiguation 1-candidate case structurally | ||
| /// unrepresentable — `AmbiguousRoot` requires ≥2 candidates by | ||
| /// construction. | ||
| /// | ||
| /// Dissolution: γ refinement and the enumerate-all rule both reuse | ||
| /// this same partition behind the `workflow_root_port` accessor; no | ||
| /// carrier change required when those rules wire. | ||
| #[derive(Debug, Clone, PartialEq, Eq)] | ||
| pub enum WorkflowRoot { | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Already fixed in working tree (commit pending). The Rust
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Already fixed at head |
||
| SingleRoot(PortId), | ||
| NoRoot, | ||
| AmbiguousRoot { | ||
| candidates: NonSingletonList<PortId>, | ||
| }, | ||
| } | ||
|
|
||
| impl Behavior { | ||
| pub fn id(&self) -> NodeId { | ||
| match self { | ||
|
|
@@ -2962,6 +2997,29 @@ impl Dag { | |
| } | ||
| } | ||
|
|
||
| /// Workflow-root accessor (Director-locked α implementation per | ||
| /// `docs/design-lens-fold-prerequisites.md` §"Prereq-3a"). Walks | ||
| /// `d.nodes` (which is topologically ordered) backwards and returns: | ||
| /// | ||
| /// - `WorkflowRoot::SingleRoot(p)` for the last `Behavior::Bind`'s | ||
| /// `result_port`, when at least one `Bind` exists. | ||
| /// - `WorkflowRoot::NoRoot` when zero `Bind` behaviors are present | ||
| /// (lens fold short-circuits to `DimensionFail`; runtime evaluation | ||
| /// rejects). | ||
| /// - `WorkflowRoot::AmbiguousRoot { .. }` is intentionally never | ||
| /// emitted by this α implementation — the linear `d.nodes` order | ||
| /// cannot tie. The variant is reserved at the type level for the | ||
| /// future enumerate-all-eligible-entries rule that R2-Evaluator's | ||
| /// `evaluate(program, entry, args)` consumes. | ||
| pub fn workflow_root_port(&self) -> WorkflowRoot { | ||
| for behavior in self.nodes.iter().rev() { | ||
| if let Behavior::Bind(b) = behavior { | ||
| return WorkflowRoot::SingleRoot(b.result_port()); | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Already fixed at head |
||
| } | ||
| } | ||
| WorkflowRoot::NoRoot | ||
| } | ||
|
|
||
| pub fn optional_match_disj(&self, cardinality_decl_id: DeclarationId) -> Option<DeclarationId> { | ||
| self.optional_match_disjs.get(&cardinality_decl_id).copied() | ||
| } | ||
|
|
@@ -3778,6 +3836,22 @@ fn duplicate_target_clean_emission_binding( | |
| mod tests { | ||
| use super::*; | ||
|
|
||
| #[test] | ||
| fn workflow_root_zero_bind_returns_no_root() { | ||
| // V3 surface syntax always lowers each top-level decl to a | ||
| // Bind, so the zero-Bind case is structurally unreachable from | ||
| // `compile_to_dag` fixtures. The α path's `NoRoot` arm is | ||
| // defensive-only at the substrate boundary; this unit test | ||
| // exercises it via the crate-private `Dag::empty()` constructor. | ||
| let dag = Dag::empty(); | ||
| let root = dag.workflow_root_port(); | ||
| assert_eq!( | ||
| root, | ||
| WorkflowRoot::NoRoot, | ||
| "Dag with no Bind behaviors must fail closed with NoRoot" | ||
| ); | ||
| } | ||
|
|
||
| fn binding_fields(language: DeclarationId, clean_emission: DeclarationId) -> ValueBody { | ||
| ValueBody::Structural { | ||
| fields: vec![ | ||
|
|
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,105 @@ | ||
| //! **Layer:** integration | ||
| //! | ||
| //! Acceptance for Prereq-3a (`workflow_root_port` accessor) per the | ||
| //! merged audit at `docs/design-lens-fold-prerequisites.md`. Director- | ||
| //! locked α implementation: last topological `Bind` in `d.nodes`. | ||
| //! | ||
| //! Three claims in this module pin the α partition over `WorkflowRoot`: | ||
| //! - `workflow_root_single_bind_returns_single_root` | ||
| //! - `workflow_root_multi_bind_returns_single_under_alpha` | ||
| //! - `workflow_root_ambiguous_unreachable_under_alpha` | ||
| //! | ||
| //! The fourth claim — `workflow_root_zero_bind_returns_no_root` — | ||
| //! lives as a unit test in `src/v3/compiler/src/dag.rs` because | ||
| //! constructing an empty `Dag` requires the crate-private | ||
| //! `Dag::empty()` constructor. | ||
| //! (renamed from the audit's `_returns_ambiguous` since linear | ||
| //! `d.nodes` cannot produce ambiguity under α; the test pins | ||
| //! that α picks the LAST Bind even with multiple Binds present). | ||
| //! | ||
| //! `WorkflowRoot::AmbiguousRoot` cannot be exercised by the α | ||
| //! implementation today; `workflow_root_ambiguous_unreachable_under_alpha` | ||
| //! pins that claim explicitly so a future enumerate-all-eligible-entries | ||
| //! rule landing under the same accessor causes the test to fail loudly, | ||
| //! forcing the rule's behavior to grow its own coverage. | ||
| //! | ||
| //! The fourth audit claim — `workflow_root_consumed_by_runtime_entry_point` | ||
| //! — is deferred to the R2-Evaluator integration PR; this slice | ||
| //! only authors the substrate accessor. | ||
|
|
||
| use crate::common::cached_compile_to_dag; | ||
| use v3_compiler::dag::{Behavior, Dag, PortId, WorkflowRoot}; | ||
|
|
||
| fn last_bind_result_port(dag: &Dag) -> PortId { | ||
| for behavior in dag.nodes().iter().rev() { | ||
| if let Behavior::Bind(b) = behavior { | ||
| return b.result_port(); | ||
| } | ||
| } | ||
| panic!("test fixture has no Bind — adjust source"); | ||
| } | ||
|
|
||
| #[test] | ||
| fn workflow_root_single_bind_returns_single_root() { | ||
| let dag = cached_compile_to_dag("let x = 1 + 2", "workflow_root_single.v3"); | ||
| let expected = last_bind_result_port(&dag); | ||
| let root = dag.workflow_root_port(); | ||
| assert_eq!( | ||
| root, | ||
| WorkflowRoot::SingleRoot(expected), | ||
| "single Bind must return SingleRoot pointing at its result_port" | ||
| ); | ||
| } | ||
|
|
||
| #[test] | ||
| fn workflow_root_multi_bind_returns_single_under_alpha() { | ||
| // Two top-level Binds in source order. Under α (last topological | ||
| // Bind), the second Bind's result_port is the workflow root. | ||
| // AmbiguousRoot is intentionally NOT emitted — it's reserved for | ||
| // the future enumerate-all-eligible-entries rule. | ||
| let dag = cached_compile_to_dag("let x = 1\nlet y = x + 2", "workflow_root_multi.v3"); | ||
| let expected = last_bind_result_port(&dag); | ||
| let root = dag.workflow_root_port(); | ||
| assert_eq!( | ||
| root, | ||
| WorkflowRoot::SingleRoot(expected), | ||
| "α picks the last topological Bind even with multiple Binds; \ | ||
| AmbiguousRoot reserved for the enumerate-all rule" | ||
| ); | ||
| } | ||
|
|
||
| #[test] | ||
| fn workflow_root_ambiguous_unreachable_under_alpha() { | ||
| // Drift trigger: under α with linear d.nodes, AmbiguousRoot is | ||
| // structurally unreachable. If a future commit makes | ||
| // workflow_root_port emit AmbiguousRoot, this test fails and | ||
| // forces the change to grow its own enumerate-all-rule coverage | ||
| // rather than silently inheriting α's tests. | ||
| let fixtures = [ | ||
| ("let x = 1", "wf_root_amb_a.v3"), | ||
| ("let x = 1\nlet y = 2\nlet z = x + y", "wf_root_amb_b.v3"), | ||
| ]; | ||
| for (src, file) in fixtures.iter() { | ||
| let dag = cached_compile_to_dag(src, file); | ||
| let root = dag.workflow_root_port(); | ||
| assert!( | ||
| !matches!(root, WorkflowRoot::AmbiguousRoot { .. }), | ||
| "fixture `{file}` produced AmbiguousRoot under α — α is a \ | ||
| single-pick rule over linear d.nodes and must never tie. \ | ||
| If this fires, an enumerate-all-eligible-entries rule has \ | ||
| been wired and the audit's ambiguous-acceptance must move \ | ||
| to its own consumer test." | ||
| ); | ||
| } | ||
| } | ||
|
|
||
| // `workflow_root_zero_bind_returns_no_root` lives as a `#[cfg(test)]` | ||
| // unit test inside `src/v3/compiler/src/dag.rs` next to | ||
| // `Dag::workflow_root_port` itself, because constructing a truly | ||
| // empty `Dag` requires the crate-private `Dag::empty()` constructor. | ||
| // V3 surface syntax always lowers each top-level decl to a `Bind`, so | ||
| // the zero-Bind case is structurally unreachable from `compile_to_dag` | ||
| // fixtures and the `NoRoot` arm is defensive-only at the substrate | ||
| // boundary. | ||
| // | ||
| // See: dag.rs `mod tests::workflow_root_zero_bind_returns_no_root`. |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -487,6 +487,73 @@ fn lane2_workflow_at(d: Dag, id: NodeId) -> WorkflowEffect? { | |
| host lane2_workflow_effect_at | ||
| } | ||
|
|
||
| // Workflow-root identification (Director-locked α; per | ||
| // `docs/design-lens-framework.md` Q-shape and merged audit | ||
| // `docs/design-lens-fold-prerequisites.md` §"Prereq-3a"). | ||
| // | ||
| // 🟡 SCAFFOLD coproduct. The three arms partition every legitimate | ||
| // `Dag` exactly once at the substrate-load boundary: | ||
| // | ||
| // - `SingleRoot(p)` — α (last topological `Bind`) selected `p` as | ||
| // the workflow-root port. Emitted whenever the Dag contains at | ||
| // least one `Bind`; multiple Binds are NOT ambiguous under α — | ||
| // the linear `d.nodes` order picks exactly one last element by | ||
| // definition. `p` is the chosen Bind's `result_port`. | ||
| // - `NoRoot` — zero `Bind` behaviors in `d.nodes`. The fold short- | ||
| // circuits (`fold_lens<C>` returns `DimensionFail` with a | ||
| // no-root diagnostic; `R2-Evaluator.evaluate(...)` rejects). | ||
| // - `AmbiguousRoot { candidates }` — reserved for the | ||
| // enumerate-all-eligible-entries rule that the runtime evaluator | ||
| // (`evaluate(program, entry, args)` per Items 4+5 / #1176 §3.2) | ||
| // consumes for multi-entry programs. The α / γ "last X Bind" | ||
| // rules cannot populate this arm over a linear `Dag.nodes` — | ||
| // both pick exactly one element by definition. Pinned here as a | ||
| // fail-closed surface for the future enumerate-all consumer | ||
| // wiring; today's α implementation never emits this variant. | ||
| // | ||
| // Pattern 1 (per-call total fact) was rejected: `-> PortId` would | ||
| // fabricate or panic on `NoRoot` cases. Pattern 2 (collapse to | ||
| // `Option<PortId>`) loses the `AmbiguousRoot` channel for the | ||
| // multi-entry consumer. Pattern 3 (this sum) is the dissolution | ||
| // path: each variant carries the structural reason its arm was | ||
| // taken; consumers dispatch fail-closed without fabrication. | ||
| // | ||
| // Dissolution: γ refinement (last `UserCallable` `Bind`) and the | ||
| // enumerate-all rule both reuse this same partition behind the | ||
| // `workflow_root_port` accessor; no carrier change required. | ||
| type WorkflowRoot | ||
| = SingleRoot(PortId) | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Already fixed in working tree (commit pending after regen). Line 527 now reads |
||
| | NoRoot | ||
| | AmbiguousRoot { candidates: NonSingletonList<PortId> } | ||
|
|
||
| // Workflow-root accessor (per merged audit Prereq-3a). Implements | ||
| // the α rule: last topological `Bind` in `d.nodes`. Returns | ||
| // `WorkflowRoot::SingleRoot(b.result_port)` when the Dag contains | ||
| // at least one Bind (α picks the last one); `NoRoot` when zero | ||
| // Binds; never `AmbiguousRoot` under α (linear `d.nodes` cannot | ||
| // tie — multiple Binds are not ambiguous, α just picks the last). | ||
| // Shared authority — both `fold_lens<C>` (workflow-root | ||
| // identification for the equivalence target) and R2-Evaluator | ||
| // (runtime entry-point identification) are the planned consumers. | ||
| // | ||
| // 🟡 BOUNDED STAGING on the realization side. The declaration + | ||
| // Rust impl + Rust binding (`rust_workflow_root_port_accessor` + | ||
| // `workflow_root_port_binding_rust` in `src/v3/spec/rust.dag`) land | ||
| // in Prereq-3a (this PR), which puts the accessor in | ||
| // `substrate_accessor_universe` so any `.dag` consumer that | ||
| // references it lowers to the Rust template. Per-target | ||
| // Python/Go bindings are NOT in this PR. Trigger: when a Python | ||
| // or Go emitter first consumes `workflow_root_port`, the | ||
| // corresponding `SubstrateAccessorBinding` lands atomically with | ||
| // that consumer — same staging discipline as `lane2_workflow_at` | ||
| // (Rust binding landed first because the lens runtime needs it; | ||
| // other targets land when they emit a consumer). Today's path | ||
| // fails closed at emit time for the unbound targets via | ||
| // `EmitError::MissingSubstrateAccessorRealization`. | ||
| fn workflow_root_port(d: Dag) -> WorkflowRoot { | ||
This comment was marked as resolved.
Sorry, something went wrong.
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Intentionally out of scope for Prereq-3a per the merged audit Prereq-3a (this slice) lands the substrate accessor + Rust impl + Rust-side consumer tests; the four acceptance tests use
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Stale finding — both items already landed in current head (post your sha). |
||
| host workflow_root_port | ||
| } | ||
|
|
||
| // `Lookup<DeclarationId>` monomorphized constructors (same shim story as | ||
| // `miss_int_lookup` in `v3.std.lookup` and `miss_symbolic_cost_lookup` in | ||
| // `std.algebra`). Lives here so `infer_helpers.dag` can call them via | ||
|
|
||
This comment was marked as resolved.
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.