Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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/crystallization/constraint-graph.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@
|---|---|---|---|---|---|
| B1 | ハンドラ探索 deep / shallow | **deep**(parent鎖を全探索、再開後もハンドラ残置) | dispatch.rs find_handler_for_effect(:247-250付近) | shallowの再設置パターン、軽量一回ハンドラ | spec(SPEC-VM-020) |
| B2 | 継続使用回数 one-shot / multi-shot | **one-shot** | continuation.rs `take()`(:284付近)、エラー "one-shot violation" | 分岐再開(amb/プロンプト再入)、リプレイ、時間旅行 | spec(SPEC-VM-021)+test |
| B3 | one-shot強制 観測(ID+flag) / 構成(move) | **構成(move)** — `Option::take`、Clone禁止 | SPEC-VM-021:84,200、違反テスト(Clone/AtomicBool禁止) | 継続の恒等子・レジストリ・共有フラグ(=v1の補償機構) | spec+test |
| B3 | one-shot強制 観測(ID+flag) / 構成(move) | **構成(move)** — `Option::take`、Clone禁止 | continuation.rs:252 `chain: Option<DetachedFiberChain>`, take():277, SPEC-VM-021:84,200, ガードテスト test_move_semantics_architecture.py(6件), D19 | 継続の恒等子・レジストリ・共有フラグ(=v1の補償機構)、Arc/Mutex/share_handle(=PR #404の機構、D19で除去) | spec+test |
| B4 | エフェクト選別 ランタイム型フィルタ / ハンドラ全受け | **全受けパターンマッチ** | SPEC-VM-020:206 | ランタイム型フィルタ最適化(キャッシュ含む) | spec ※残骸あり(§4-①) |
| B5 | ハンドラ解決 evidence passing / 動的探索 | **動的探索**(毎perform、キャッシュなし) | dispatch.rs(キャッシュ構造なし)、SPEC-VM-020:206がキャッシュ禁止 | 設置時解決、O(1)ディスパッチ | **成り行き**(evidence passingは未検討 [owner])。高速Rust化の論点として保留 |
| B6 | 状態×継続 共有 / スナップショット | **共有**(cells捕獲時コピーなし) | src/var_store.rs、vm/var_store.rs(コピー箇所なし) | 分岐意味論、トランザクショナルロールバック、multi-shot拡張 | **owner: 意図的・確定**(one-shot前提で共有が正しい)。law未明文 → Task 4で昇格。SPEC-EFF-002のknown issue(gh#157 snapshot isolation)は本回答と矛盾、spec更新要。※追記: `global_state`/`writer_log`は呼び出し元ゼロの死設備と判明(§4-④)。**※2026-06-12訂正: cells(Var)もスコープ束縛も死設備**(D15 — Python到達経路なし)。VM特権状態はゼロで、B6の共有意味論はPythonクロージャハンドラの状態(scheduler/state/writer)についてのlawとして生きる。正統のState/Writerハンドラはクロージャ実装(algebra-draft.md §0) |
Expand Down
8 changes: 8 additions & 0 deletions docs/crystallization/decision-records.md
Original file line number Diff line number Diff line change
Expand Up @@ -112,3 +112,11 @@
- **選択**: lawは「全ハンドラについての定理」ではなく「ハンドラ契約」(理論T、ハンドラ=T-代数の標準観)。契約を満たすハンドラだけが生成元名(Reader/State/Writer等)を名乗れる
- **理由**: 「Askを数えてTellするハンドラ」のような効果的ハンドラはA1/A4の見かけ反例になるが、これは代数の欠陥ではなく記述の欠陥。再解釈でA系・S系・W系への同型攻撃が全てハンドラ側の義務に転化する
- **帰結**: 等式変形(人・codexのリファクタリング)の正当性は「設置ハンドラの契約準拠」を前提とする、と規格に明記(algebra-draft §3冒頭)

## D19. K1復元: PR #404のArc/share_handle機構を除去し、move-only法を復元 [オーナー — 2026-06-12]

- **選択**: Option (b) — 構成的move-only法を復元。PR #404のArc<Mutex<Option<>>>・share_handle機構を完全に除去し、Continuation.chainを`Option<DetachedFiberChain>`(plain move)に戻す。例外伝播の#404セマンティクスは`Py<PyK>`ハンドル(Python参照、継続コピーではない)で保持
- **棄却**: Option (a) — 仕様を弱めてArc機構を許容(K1結合核の法を放棄することに等しい)
- **理由**: PR #404(47d2a518, 2026-04-25)は実際の意味論バグを修正したが、選ばれた機構がSPEC-VM-021不変条件1, 2, 4に違反。share_handle()はArcの第二参照を生成、VMとFrameに`Option<Continuation>`バックアップを格納。さらにライブバグ: バックアップがone-step窓を超えて残存し、次の無関係なProgramフレームに付着(stale-backup-leak)
- **機構**: VMは`Py<PyK>`ハンドル(continuation.rsのPyKへのPython参照)を保持。ハンドラが例外を発生させた場合、VMはハンドルを借用してPyK.take()でチェーンを取得し再接続(discontinue k exn相当)。Callable traitに`is_generator_handler()`を追加: Pythonジェネレータハンドラのみ`Py<PyK>`バックアップを使用、同期Rustハンドラは`Value::Continuation(k)`を直接受け取る
- **検証**: #404回帰テスト6件全件green、stale-backup-leak回帰テスト追加、ガードレイヤー(test_move_semantics_architecture.py)をSPEC-VM-021不変条件に準拠するよう書き直し(6テスト全pass)、cargo test --features "python_bridge,invariant-checks" 37pass/0fail
129 changes: 29 additions & 100 deletions packages/doeff-vm-core/src/continuation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,18 +6,17 @@
//!
//! Parent pointers in the arena are the source of truth for chain structure.
//! Continuation owns detached fibers directly while they are outside the arena.
//! One-shot via `lock().take()` — destructive read, like OCaml 5's atomic_swap.
//! One-shot via `Option::take()` — destructive read, like OCaml 5's atomic_swap.
//!
//! ## Shared cell ownership
//! ## Move-only ownership (SPEC-VM-021 invariant)
//!
//! The internal storage is `Arc<Mutex<Option<DetachedFiberChain>>>` so the VM
//! can hold a backup handle while a `Continuation` is on loan to a handler
//! callable (Python). If the handler raises before consuming `k`, the VM
//! recovers the chain through the backup handle and routes the exception to
//! the original perform site. One-shot is preserved by the lock+take pattern:
//! whoever takes first wins; the loser sees `None`.

use std::sync::{Arc, Mutex};
//! The chain lives directly in `Option<DetachedFiberChain>` — no Arc, no Mutex.
//! At every instant the DetachedFiberChain has EXACTLY ONE owning location
//! (the PyK value, a frame slot, or in-flight move). One-shot is enforced by
//! construction: `Option::take()` returns `Some` first time, `None` after.
//! The VM does not store continuations; for exception recovery during handler
//! dispatch, it keeps a `Py<PyK>` reference (a Python handle, not a
//! continuation) — see vm.rs `pending_handler_k_handle`.

use pyo3::prelude::*;
use pyo3::types::PyDict;
Expand Down Expand Up @@ -238,22 +237,19 @@ impl DetachedFiberChain {
// Continuation — the detached fiber chain
// ---------------------------------------------------------------------------

/// A captured fiber chain. NOT Clone publicly — one semantic owner, one-shot.
/// A captured fiber chain. NOT Clone — one semantic owner, one-shot.
///
/// Internally the chain lives in `Arc<Mutex<Option<DetachedFiberChain>>>` so
/// the VM can hold a backup handle while the Continuation is loaned to a
/// handler (see `share_handle`). One-shot is preserved by the lock+take
/// pattern: only one caller can `take()` the chain; subsequent takes return
/// `None`.
/// The chain lives directly in `Option<DetachedFiberChain>` — move-only by
/// construction. `Option::take()` enforces one-shot: Some first time, None
/// after. No Arc, no Mutex, no shared handles (SPEC-VM-021 invariants 1–4).
///
/// Created by `perform` (detach chain from handler).
/// Consumed by `reattach_chain` / `continue_k` (reattach chain to caller).
/// Extended by `reperform` (append current fiber to chain).
#[derive(Debug)]
pub struct Continuation {
/// Shared cell holding the detached fiber chain.
/// `lock().take()` enforces one-shot: Some first time, None after.
chain: Arc<Mutex<Option<DetachedFiberChain>>>,
/// The detached fiber chain. Some = live, None = consumed.
chain: Option<DetachedFiberChain>,
}

impl Continuation {
Expand All @@ -262,81 +258,44 @@ impl Continuation {
pub fn from_chain(chain: DetachedFiberChain) -> Self {
memory_stats::register_continuation();
Self {
chain: Arc::new(Mutex::new(Some(chain))),
chain: Some(chain),
}
}

/// Sentinel for an already-consumed continuation (head=None).
/// Sentinel for an already-consumed continuation (chain=None).
/// Used by the Python bridge when PyK has already been taken.
/// The VM core's reattach_chain will detect this and raise the one-shot
/// error with full VM context (current_segment, traceback).
pub fn empty() -> Self {
// Register so Drop's unregister is balanced.
memory_stats::register_continuation();
Self {
chain: Arc::new(Mutex::new(None)),
}
Self { chain: None }
}

/// One-shot take: returns the detached chain and clears the cell.
/// If a backup handle (via `share_handle`) was created, this take is
/// observed by the backup as well — the cell becomes None for everyone.
/// First call returns `Some(chain)`, subsequent calls return `None`.
pub fn take(&mut self) -> Option<DetachedFiberChain> {
self.chain
.lock()
.expect("Continuation chain mutex poisoned")
.take()
}

/// Create a backup handle pointing at the same chain cell.
///
/// Used by the VM during handler invocation: before passing a Continuation
/// to the handler callable, the VM keeps a `share_handle` so that, if the
/// handler raises before consuming `k`, the chain can be recovered through
/// the backup. The lock+take pattern guarantees one-shot: whichever side
/// (handler or VM) takes first wins; the other sees `None`.
///
/// Crate-internal — handler/user code must NOT call this. Cloning at the
/// public API surface would violate the single-owner contract.
pub(crate) fn share_handle(&self) -> Self {
memory_stats::register_continuation();
Self {
chain: Arc::clone(&self.chain),
}
self.chain.take()
}

/// Head fiber (identity of this continuation).
pub fn head(&self) -> Option<FiberId> {
self.chain
.lock()
.expect("Continuation chain mutex poisoned")
.as_ref()
.map(DetachedFiberChain::head)
self.chain.as_ref().map(DetachedFiberChain::head)
}

/// Last fiber in the chain.
pub fn last_fiber(&self) -> Option<FiberId> {
self.chain
.lock()
.expect("Continuation chain mutex poisoned")
.as_ref()
.map(DetachedFiberChain::last_fiber)
self.chain.as_ref().map(DetachedFiberChain::last_fiber)
}

/// Is this continuation already consumed?
pub fn consumed(&self) -> bool {
self.chain
.lock()
.expect("Continuation chain mutex poisoned")
.is_none()
self.chain.is_none()
}

/// Is this a live (unconsumed) continuation?
pub fn is_live(&self) -> bool {
self.chain
.lock()
.expect("Continuation chain mutex poisoned")
.is_some()
self.chain.is_some()
}

/// Identity = head fiber. Used as dispatch identity.
Expand All @@ -345,58 +304,28 @@ impl Continuation {
}

pub(crate) fn append_chain(&mut self, chain: DetachedFiberChain) -> bool {
let mut guard = self
.chain
.lock()
.expect("Continuation chain mutex poisoned");
let Some(existing) = guard.as_mut() else {
let Some(existing) = self.chain.as_mut() else {
return false;
};
existing.append(chain);
true
}

pub fn collect_traceback(&self) -> Option<Vec<StreamSourceLocation>> {
self.chain
.lock()
.expect("Continuation chain mutex poisoned")
.as_ref()
.map(DetachedFiberChain::collect_traceback)
self.chain.as_ref().map(DetachedFiberChain::collect_traceback)
}

pub fn handler_callables(&self) -> Option<Vec<CallableRef>> {
self.chain
.lock()
.expect("Continuation chain mutex poisoned")
.as_ref()
.map(DetachedFiberChain::handler_callables)
self.chain.as_ref().map(DetachedFiberChain::handler_callables)
}

pub fn collect_rich_context(&self) -> Option<Vec<Value>> {
self.chain
.lock()
.expect("Continuation chain mutex poisoned")
.as_ref()
.map(DetachedFiberChain::collect_rich_context)
}
}

#[cfg(feature = "invariant-checks")]
impl Continuation {
/// Pointer identity of the shared chain cell. Backup handles created via
/// `share_handle` report the same address — used by the invariant checker
/// to deduplicate cells before locking (avoids double-count and re-lock).
pub(crate) fn cell_addr(&self) -> usize {
Arc::as_ptr(&self.chain) as usize
self.chain.as_ref().map(DetachedFiberChain::collect_rich_context)
}

/// Inspect the current chain contents without consuming (None = consumed).
pub(crate) fn inspect_chain<R>(&self, f: impl FnOnce(Option<&DetachedFiberChain>) -> R) -> R {
let guard = self
.chain
.lock()
.expect("Continuation chain mutex poisoned");
f(guard.as_ref())
f(self.chain.as_ref())
}
}

Expand Down
27 changes: 14 additions & 13 deletions packages/doeff-vm-core/src/frame.rs
Original file line number Diff line number Diff line change
Expand Up @@ -183,16 +183,17 @@ pub enum Frame {
Program {
stream: IRStreamRef,
metadata: Option<CallMetadata>,
/// Backup handle on the original perform-site continuation, used
/// only for handler-body program frames. If this stream raises an
/// uncaught exception, the VM reattaches `chain_backup`'s chain and
/// raises into the resulting stream so the inner handler's `<-`
/// site (or the user program's perform site) can `try/except` the
/// error. None for ordinary program frames (user body, etc.).
/// Reference to the PyK Python object that owns the perform-site
/// continuation chain, used only for handler-body program frames.
/// If this stream raises an uncaught exception, the VM borrows this
/// handle, takes the chain from the PyK (if the handler didn't
/// consume k), and reattaches it so the inner handler's `<-` site
/// (or the user program's perform site) can `try/except` the error.
/// None for ordinary program frames (user body, etc.).
///
/// One-shot is preserved by `Continuation::take` (lock+take); the
/// handler's own PyK shares the same chain cell.
chain_backup: Option<crate::continuation::Continuation>,
/// This is a Python handle (Py<PyK>), NOT a continuation. The chain
/// lives inside the PyK — move-only by construction (SPEC-VM-021).
handler_k_handle: Option<pyo3::Py<crate::continuation::PyK>>,
},
LexicalScope {
bindings: HashMap<HashedPyKey, Value>,
Expand All @@ -215,19 +216,19 @@ impl Frame {
Frame::Program {
stream,
metadata,
chain_backup: None,
handler_k_handle: None,
}
}

pub fn program_with_backup(
pub fn program_with_k_handle(
stream: IRStreamRef,
metadata: Option<CallMetadata>,
chain_backup: Option<crate::continuation::Continuation>,
handler_k_handle: Option<pyo3::Py<crate::continuation::PyK>>,
) -> Self {
Frame::Program {
stream,
metadata,
chain_backup,
handler_k_handle,
}
}

Expand Down
10 changes: 10 additions & 0 deletions packages/doeff-vm-core/src/value.rs
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,16 @@ pub trait Callable: Send + Sync + std::fmt::Debug + 'static {
None
}

/// Whether this callable runs as a multi-step generator handler.
/// Generator handlers (e.g., Python `@do` generators) need a `Py<PyK>`
/// backup handle for exception recovery across yields. Synchronous
/// handlers (`call_handler` returns immediately with a complete `DoCtrl`)
/// don't need a backup — the continuation is consumed by the returned
/// `DoCtrl` or freed on drop.
fn is_generator_handler(&self) -> bool {
false
}

/// Downcast support for bridge layer (e.g., extracting PythonCallable).
fn as_any(&self) -> &dyn std::any::Any;
}
Expand Down
21 changes: 13 additions & 8 deletions packages/doeff-vm-core/src/vm.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30,11 +30,16 @@ pub struct VM {
pub var_store: VarStore,
pub current_segment: Option<SegmentId>,
/// Transient slot used by `eval_perform`/`eval_perform_with_k` to thread
/// the chain backup through to the next `push_stream_value` call. Set
/// before calling a handler callable; consumed when the resulting Stream
/// frame is pushed (the backup ends up in `Frame::Program.chain_backup`).
/// Always None outside that narrow window.
pub pending_handler_chain_backup: Option<crate::continuation::Continuation>,
/// a reference to the handler's PyK object through to `push_stream_value`.
/// Set before calling a handler callable; consumed when the resulting
/// Stream frame is pushed (the handle ends up in
/// `Frame::Program.handler_k_handle`).
///
/// This is a Python handle (Py<PyK>), NOT a continuation. The chain lives
/// inside the PyK — if the handler raises, the VM borrows this handle,
/// calls `PyK::take()`, and reattaches the recovered chain.
/// Always None outside the handler-dispatch window.
pub pending_handler_k_handle: Option<pyo3::Py<crate::continuation::PyK>>,
}

impl VM {
Expand All @@ -43,15 +48,15 @@ impl VM {
segments: FiberArena::new(),
var_store: VarStore::new(),
current_segment: None,
pending_handler_chain_backup: None,
pending_handler_k_handle: None,
}
}

pub fn begin_run_session(&mut self) {
self.segments.clear();
self.var_store.clear_run_local();
self.current_segment = None;
self.pending_handler_chain_backup = None;
self.pending_handler_k_handle = None;
}

pub fn end_active_run_session(&mut self) {
Expand All @@ -60,7 +65,7 @@ impl VM {
self.var_store.clear_run_local();
self.var_store.shrink_run_local_to_fit();
self.current_segment = None;
self.pending_handler_chain_backup = None;
self.pending_handler_k_handle = None;
}

pub fn alloc_segment(&mut self, fiber: Fiber) -> FiberId {
Expand Down
Loading
Loading