Skip to content

Make ephemerality provenance-tracked and modular #362

@ehartford

Description

@ehartford

Summary

The spec now states that ephemerality is not purely structural. Type-level ephemerality is structural, but value-level ephemerality is provenance-tracked: returned-origin sets, binding-level task ephemerality, closure/callable capture provenance, assignment/call propagation, returned-view checking, and escape checks require deterministic compiler analysis.

This issue tracks completing that implementation substrate. The goal is not Rust-style user lifetime annotations. The compiler carries the facts so the user does not have to.

Root cause / 5 Whys

  1. Why was the old requirement wrong? It said no dataflow was required and that ephemerality was determined structurally by types.
  2. Why is that unsound? Returned references/views, task handles, closures, and callable values need to know which origin a value came from, not merely what shape its type has.
  3. Why can't type shape answer that? Task[T] has one spelling whether ephemeral or non-ephemeral, and a returned &T may originate from a parameter, receiver, capture, static storage, or local temporary.
  4. Why do we need summaries? The checker must remain modular across function, closure, function-pointer, trait-object, wrapper, and call boundaries without user-written lifetime syntax.
  5. Root cause: With needs a unified deterministic value-provenance summary/dataflow substrate. The implementation has partial machinery, but the spec-level model is broader than the current ad hoc checks.

Current implementation evidence

Partial machinery already exists:

  • src/Sema.w carries signature returned-view origin masks (sig_param_view_origins), binding view deps, expression view deps, closure capture summaries, and task ephemerality binding state.
  • src/SemaCheck.w has returned/yielded view origin checks around check_returned_view_origins, record_call_view_origins, and check_return.
  • src/SemaCheck.w tracks ephemeral task creation/storage through expr_creates_ephemeral_task, expr_is_ephemeral_task, check_ephemeral_task_arg_escape, and check_ephemeral_task_storage.
  • src/SemaCheck.w rejects escaping closures that capture ephemeral references and records closure capture summaries.
  • Existing compile-error fixtures cover some direct cases: err_return_local_ref_direct.w, err_return_local_ref_via_call.w, err_return_local_ref_binding.w, err_escaping_bound_closure_captures_ref.w, err_thread_spawn_closure_captures_ref.w, and several ephemeral-task storage/escape fixtures.

Required design shape

  • Preserve structural type-level ephemerality for references, declared-ephemeral types, and aggregates/generic containers with ephemeral components.
  • Add or complete value-level provenance facts for bindings, returned-origin sets, task captures, closure captures, assignment propagation, call propagation, returned views, and escape checks.
  • Task[T] keeps one spelling. A task value is ephemeral when its captures/result depend on an ephemeral origin; this is inferred and propagated.
  • Closures and callable values carry summaries: captures, origin sets, ephemerality, and may_suspend facts across closure, function pointer, trait object, generated-wrapper, and indirect-call boundaries.
  • The analysis is modular: intra-procedural dataflow plus inferred summaries at interfaces.
  • The analysis is deterministic and conservative. No unordered map iteration or pointer-address ordering may affect verdicts. If safety cannot be proven, reject.
  • False rejection of actually-safe code is compiler precision debt, not a reason to add user lifetime/ephemerality annotations.

Acceptance criteria

  • Tests cover direct returned local reference/view escapes and safe parameter/static-origin returns.
  • Tests cover origin propagation through local bindings, assignments, and function calls.
  • Tests cover ephemeral task capture propagation through binding, assignment, storage, send/detach, callback, and return paths.
  • Tests cover closure/callable summary propagation, including function pointers or trait-object/dyn callables if those surfaces exist.
  • Diagnostics name the escaping value and the origin/provenance fact that could not be proven safe.
  • with build, with build :fixpoint, with build :test, and with build :test-green pass.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions