reentrance: enter-sync-call checks the callee gate but never takes it — host-mediated reentry passes where the reference traps

[lannbot]

From the 2026-08-20 conformance review (five independent tracks against the pinned definitions.py; companion fixes: PR #164).

The divergence

enter-sync-call (runtime/src/intrinsics/mod.ts ~513-536) performs the reference's reentrance check but never takes the gate: it runs trap_if(!calleeInst.mayEnterFrom(callerInst)) and stops. The reference brackets the whole call — Store.lift (definitions.py:578-585): trap_if(not inst.may_enter_from(caller)), then enter_from(caller) … leave_to(caller). The in-code comment documents the omission as deliberate ("Reported, not smuggled in", pointing at task/mod.ts enteringSet).

The documented equivalence argument covers guest-initiated reentry only: a pure guest→guest cycle is statically impossible (FACT compiles same-instance/ancestor calls to compile-time traps; sibling cycles unreachable because instance imports form a DAG — the #99/#101 adjudication), which is also why wasmtime elides the runtime check entirely.

The uncovered window is host-mediated reentry: host → A.f → sync FACT adapter → C.g → C calls a host import → the host synchronously (or while C is parked) re-enters C.g. Because the sync adapter never marked C entered, createLiftedFunction's host gate sees C enterable and admits the call; the reference traps cannot enter component instance (C is in the first call's entered set).

Ask

Adjudicate one of:

1. Take the bracket: enter-sync-call does enterFrom(callerInst) and exit-sync-call releases, with the trap-path discipline mirrored from the other bracket sites (trap ⇒ bracket stays broken + notifyInstancePoisoned; capability signal ⇒ release). Restores reference behavior; needs care with the existing sync-call-stack unwind paths.
2. Document the acceptance: record host-mediated-reentry-during-sync-adapter-call as a named divergence (wasmtime parity — it elides the check; definitions.py is nominally the tie-breaker, so this needs an explicit adjudication note in docs/architecture.md rather than a code comment alone).

Classification from the review: C (documented divergence, equivalence argument incomplete for the host-mediated case), high confidence on semantics.

[lannbot]

Adjudicated: accept (the bracket stays omitted). Recorded as a named divergence in docs/architecture.md §6 via #174. Deciding grounds, in order of force: upstream is deleting the restriction outright — CM#705 removes the may_enter flag/trap from the canon lift/resource.drop/subtask.cancel paths and makes previously-trapping reentrance valid — so option 1 would implement enforcement with an expiry date; wasmtime parity (it never performed this check); and taking the bracket would create a guest→guest lock spanning suspension points, reintroducing the await-spanning-lock class #156/#160 eliminated. Self-resolves at the submodule pin advance; the migration map for everything #705 obsoletes in deltic is #173. Closed by #174 on merge.