Lower branch-yield result joins into Core - #194
Conversation
|
Important Review skippedAuto reviews are disabled on base/target branches other than the default branch. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Pro Plus Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ab765f9ac9
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
# Conflicts: # docs/topics/compiler-spine/test-plan.md
|
@codex review please |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: bae3229e52
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
@codex review please |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4eff0c0fb6
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
@codex review please |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f3aeab2603
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
@codex review please |
|
Codex Review: Didn't find any major issues. Nice work! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
|
@codex review please |
|
Codex Review: Didn't find any major issues. Keep them coming! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
Summary
letexpressions into isolated Core blocks with one joined result;This PR is stacked on #193 and is another bounded part of #192. It does not close #192 or claim Target IR/runtime execution.
Plain-English Walkthrough
TL;DR
Edict can now preserve the meaning of
let x = if predicate { ... yield a; } else { ... yield b; };in Core without evaluating either branch in the compiler and without adding a host callback. [claim:branch-yield-core, confidence:1.00] Each branch remains an isolated Core block; exactly the selected block runs; its result becomes one explicit outer local; and incompatible yielded types fail during type checking.Walkthrough
The preceding PR introduced target-neutral Core branch blocks, but those blocks had no way to name the selected result. That was sufficient for statement-only
if, whose blocks returnNull, but insufficient for the language's branch-yield form.This change makes the distinction explicit:
ifNulllet[claim:optional-branch-binding, confidence:1.00] The optional binding is part of the normative Core CDDL, Rust model, canonical encoder, CLI review projection, and generated provider contract pack.
The compiler dataflow is:
flowchart TD A[Branch-yield let] --> P[Type-check pure predicate] P --> T[Lower then block in isolated scope] P --> E[Lower else block in isolated scope] T --> J{Yielded types compatible?} E --> J J -->|No| R[Structured TypeMismatch] J -->|Yes| B[Allocate one outer result local] B --> C[Emit bound Core branch]Caption: Explicit branch-result join
The join is semantic structure, not runtime policy. The current Target IR lowerer continues to reject Core branch nodes, so this PR gives downstream work honest compiler-produced input without claiming that Echo can execute it yet.
Branch-local effects use only the already-supported typed effect-call path and obstruction mapping. [claim:branch-scope, confidence:1.00] Branch locals do not leak into the enclosing environment; only the explicit result binding does. Bare effect statements, new intrinsics, application-specific operations, and host callbacks remain unsupported.
Branch-yield profile admission now runs before its specialized lowering path. [claim:branch-effect-profile-gate, confidence:1.00] A coordinate that appears in both pure-helper and write-effect facts cannot bypass its operation-profile write-class gate; a disallowed write class returns
ProfileEffectMismatchbefore Core.Canonical identity covers the new meaning. [claim:branch-binding-identity, confidence:1.00] Tests show that swapping compatible yielded values changes the Core digest, and removing only the result binding also changes the Core digest.
Verification
The authority-gate RED command was:
Before the fix, that source incorrectly produced Core. It now returns exactly
ProfileEffectMismatch.The original focused RED command was:
Before implementation, it failed because
CoreNode::Branchhad nobindingfield. After implementation, all three focused branch-yield cases passed.The first full gate correctly found two contract-boundary obligations: an invalid topic-source registry reference and provider contract-pack drift after the Core CDDL change. The registry reference was removed, and the generated pack was refreshed through its owner:
The parallel fixture calibration and final complete gates passed:
[claim:full-verification, confidence:1.00] This includes formatting, clippy, all workspace tests, Core schema checks, provider contract-pack reproduction, doctests, and golden checks.
Compatibility, dependencies, and documentation
No dependency was added. Adding a field to the public Rust
CoreNode::Branchvariant requires downstream exhaustive destructuring to account forbinding; in-repository consumers were updated. The CDDL field is optional, preserving the existing representation for statement-only branches. Compiler-spine and Core IR shelves now document the distinction and the remaining Target IR boundary.Appendix: Citations
claim:branch-yield-corecrates/edict-syntax/src/compiler.rs#1725@244a6645e61308b616b8675706fe3c16be0ccba1;effectful_branch_yield_lowers_to_bound_core_branchincrates/edict-syntax/tests/compiler_spine.rsclaim:optional-branch-bindingdocs/abi/edict-core.cddl#308@244a6645e61308b616b8675706fe3c16be0ccba1;crates/edict-syntax/src/core_ir.rs#315@244a6645e61308b616b8675706fe3c16be0ccba1;crates/edict-syntax/src/canonical.rs#1098@244a6645e61308b616b8675706fe3c16be0ccba1claim:branch-scopecrates/edict-syntax/src/compiler.rs#1785@244a6645e61308b616b8675706fe3c16be0ccba1;effectful_branch_yield_lowers_to_bound_core_branchincrates/edict-syntax/tests/compiler_spine.rsclaim:branch-binding-identityeffectful_branch_yield_mutation_moves_core_digestincrates/edict-syntax/tests/compiler_spine.rs#992@244a6645e61308b616b8675706fe3c16be0ccba1claim:branch-effect-profile-gatecrates/edict-syntax/src/compiler.rs#1653;branch_yield_rejects_pure_helper_that_is_a_disallowed_write_effectincrates/edict-syntax/tests/compiler_spine.rs#969claim:full-verificationcargo xtask verifyat244a6645e61308b616b8675706fe3c16be0ccba1(passed locally)Part of #192