Prove stale process refs preserve runtime identity#100
Merged
Conversation
Add a source-to-runtime gate that spawns two same-definition workers, transports the first ProcessRef through another process, stops that original PID, and proves the follow-up send returns Err(Stopped(Work)) instead of retargeting to the later worker. Wire the example into runnable gates, assurance markers, and documentation so the runtime boundary remains documented and testable. Constraint: Process references are runtime authority surfaces that must dispatch through typed process IDs and runtime PIDs rather than source names. Rejected: Source-name or type-spelling dispatch checks alone | trace-level PID assertions are required to prove non-retargeting. Confidence: high Scope-risk: narrow Directive: Keep stale ProcessRef behavior tied to runtime PID identity; update trace-level gates if scheduler or PID lifecycle semantics change. Tested: just process-ref-lifecycle-gates; just run-example process_ref_stale_lifecycle; just language-surface-assurance; just source-to-runtime-gates; just quality; just performance-smoke; just fuzz-ci; just miri-ci Not-tested: Long-duration stress or OS-level RSS profiling beyond existing performance-smoke and fuzz/Miri gates.
There was a problem hiding this comment.
Pull request overview
This PR adds an executable “source-to-runtime” gate proving that transported (stale) ProcessRef<Worker> values remain bound to their original runtime PID and do not retarget to a newer instance of the same process definition.
Changes:
- Added a new runnable example (
process_ref_stale_lifecycle) that transports a staleProcessRef<Worker>through aSenderand asserts the later send yieldsErr(Stopped(Work)). - Added/ wired an acceptance-test gate (including trace + artifact assertions) and integrated it into
just source-to-runtime-gatesplus the success-example list. - Updated docs and language-surface assurance markers to make the stale-ref identity guarantee visible and tracked.
Reviewed changes
Copilot reviewed 8 out of 8 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
Justfile |
Adds a focused process-ref-lifecycle-gates recipe and wires it into source-to-runtime-gates; includes the example in the success gates list. |
examples/process_ref_stale_lifecycle.str |
New example exercising stale ProcessRef lifecycle behavior via a transported reference and stopped-send outcome. |
docs/src/source-to-runtime-gates.md |
Documents the new runnable example and the dedicated lifecycle gate + its trace-level proof intent. |
docs/src/runtime-reference.md |
Updates process-reference boundary text to explicitly state transported refs never retarget to newer instances. |
docs/src/examples.md |
Adds the new example to the recommended reading order list. |
docs/src/examples-runtime.md |
Adds a runtime-focused bullet describing what the new example proves. |
crates/strata-mantle-acceptance/tests/source_to_runtime_gates/process_refs_and_authority.rs |
Adds the acceptance test validating stdout signals, artifact lowering shape, and trace evidence for stale-ref non-retargeting. |
crates/strata-mantle-acceptance/tests/language_surface_assurance/process.rs |
Wires the new example + test into the language-surface assurance feature matrix. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
The stale ProcessRef gate must prove a newer same-definition worker exists before the stale send outcome is bound, not merely that both events occurred somewhere in the trace. Reusing the existing trace line-index helper keeps the assertion exact and source-to-runtime focused. Constraint: PR review identified a trace-order proof gap in the stale ProcessRef lifecycle gate. Rejected: Relying on stdout order or event presence alone | those checks do not prove the newer worker existed before the stale send outcome. Confidence: high Scope-risk: narrow Directive: Keep process-ref identity tests tied to runtime PID ordering evidence, not process/source names. Tested: cargo +stable fmt --all --check; just process-ref-lifecycle-gates; just language-surface-assurance; just source-to-runtime-gates Not-tested: Full workspace quality after this test-only assertion change.
The stale ProcessRef lifecycle gate should prove runtime identity through artifact-derived process IDs and stable assurance markers. This keeps the test aligned with the typed Strata/Mantle boundary while avoiding brittle ordering literals or assertion-message marker text. Constraint: PR review identified hardcoded process IDs and a brittle assurance marker in the stale ProcessRef proof. Rejected: Keeping current literal process_id checks | they couple the gate to artifact ordering even though the typed ID is already available. Rejected: Keeping assertion text as assurance evidence | marker wording can change without changing behavior. Confidence: high Scope-risk: narrow Directive: Keep lifecycle proof checks tied to artifact-derived typed IDs and stable test names. Tested: cargo +stable fmt --all --check; just process-ref-lifecycle-gates; just language-surface-assurance; just source-to-runtime-gates Not-tested: Full workspace quality after this narrow review-fix patch.
beardedeagle
force-pushed
the
stale-process-ref-lifecycle-gate
branch
from
43b513d to
766c1ba
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This change adds a source-to-runtime gate for stale process-reference lifecycle behavior. The new example spawns two
Workerinstances from the same process definition, transports the firstProcessRef<Worker>through aSender, stops that original runtime PID, and proves a later send through the stale reference returnsErr(Stopped(Work))instead of retargeting to the newer worker instance.What changed
examples/process_ref_stale_lifecycle.stras a runnable source-to-runtime example for stale process-reference sends.Workdelivery to the newer worker.just source-to-runtime-gatesand the runnable success-example list.Why
Process references are runtime authority surfaces. A transported reference must remain bound to the specific runtime process instance it denotes. It must not be resolved later by source process name, type spelling, or any other metadata that could accidentally route a stale reference to a newer instance of the same process definition.
This gate makes that boundary executable and trace-checked.
Validation
just process-ref-lifecycle-gatesjust run-example process_ref_stale_lifecyclejust language-surface-assurancejust source-to-runtime-gatesjust qualityjust performance-smokejust fuzz-cijust miri-cigit diff --check