A Merry Source Calling a Sandbox-Denied Kfun Errors on First Fire

Claim

In the eOS-Harness MVA running against DGD 1.7.9 plus the eOSContinuum/eOS-kernellib feature/cohesive-lift branch carrying the kernel-layer cohesive lift (Vault + Schema + XML + Index + Merry + property-change dispatcher), a Merry reaction whose source calls a sandbox-denied kfun compiles and binds without error but throws on its first invocation, and the denied operation does not occur. The dispatch shape is: the boot-time chat-app test driver compiles write_file("/usr/Chat/data/hack.txt", "pwned"); via new_object("/usr/Merry/data/merry", source) and binds the resulting script object on room_a under the reaction-property key merry:on:chat-room.intrusion:main. The registration (compile + bind) succeeds: the Merry compiler resolves write_file to the local SANDBOX(write_file) shadow method defined in merrynode.c, which exists, so the symbol is found and the script binds. The error fires only on the first invocation via run_merry, when the shadow body runs and raises function 'write_file' not allowed in merry code. The driver's catch{} converts the throw into a SANDBOX-REJECT OK sentinel and confirms no hack.txt was created. The boundary is enforced at execution, not at load: an untrusted author cannot tell at registration time whether their reaction will be stopped, because the deny is a runtime-fire deny.

Grounds

This is an Empirical Observation. The grounds are a captured cold-boot smoke run 2026-05-30 against the live MVA demonstration instance with examples/chat-app/ overlaid at the isolated runtime staging tree's src/usr/Chat/. Same boot and same setup as the paired positive Observation.

Setup (verifiable from repo state):

Driver: DGD 1.7.9 built from dworkin/dgd; binary symlinked at the isolated runtime staging tree's bin/dgd.
Kernel layer: eOSContinuum/eOS-kernellib on feature/cohesive-lift at HEAD a55b77f.
Application layer: examples/chat-app/, deployed into the isolated runtime staging tree at src/usr/Chat/.
Runtime config: the instance config; the isolated runtime staging tree layout.

Load-bearing source (phase 4 of examples/chat-app/sys/test.c):

object reject_script;

reject_script = new_object(MERRY_DATA,
        "write_file(\"" + HACK_FILE + "\", \"pwned\");");
room_a->set_property("merry:on:chat-room.intrusion:main", reject_script);
/* (the compile + bind above are in their own catch{}; a throw there
 *  is a FAIL -- registration is supposed to succeed) */

catch(remove_file(HACK_FILE));
rejected = 0;
catch {
    run_merry(room_a, "chat-room.intrusion:main", "on", ([ ]));
} : {
    rejected = 1;
}
if (!rejected) {
    log_line("ChatApp:test: FAIL: SANDBOX-REJECT denied kfun did not throw");
    return;
}
if (file_info(HACK_FILE)) {
    log_line("ChatApp:test: FAIL: SANDBOX-REJECT forbidden write created a file");
    return;
}

HACK_FILE is /usr/Chat/data/hack.txt. The shadow that fires is defined in src/usr/Merry/lib/merrynode.c via the SANDBOX(f) macro: # define SANDBOX(f) mixed f(mixed args...) { error("function '" + #f + "' not allowed in merry code"); }, with SANDBOX(write_file) among the 51 entries.

Smoke transcript (the sentinel result log after the cold boot):

ChatApp:test: starting
ChatApp:test: CAP-REJECT OK
ChatApp:test: CAP-ACCEPT OK
ChatApp:test: SANDBOX-ACCEPT OK
ChatApp:test: SANDBOX-REJECT OK

Boot-log evidence of the deny mechanism (the [caught] error and its call stack):

** function 'write_file' not allowed in merry code [caught]
                      /usr/Chat/sys/test
  123   setup_and_run    /usr/Chat/sys/test
  288 * run_tests        /usr/Chat/sys/test
  103   run_merry        /usr/Merry/lib/merryapi
                      /usr/Merry/data/merry#-1
  299   evaluate         /usr/Merry/data/merry
                      /usr/Merry/merry/<hash>
   73   evaluate         /usr/Merry/lib/merrynode
    6   merry            /usr/Merry/merry/<hash>
  448   write_file       /usr/Merry/lib/merrynode

The stack terminates at merrynode.c line 448 (the SANDBOX(write_file) shadow), reached through the compiled merry program, merrynode::evaluate, merryapi::run_merry, and the test driver's run_tests. The [caught] annotation confirms the throw was caught by phase 4's catch{} (the expected outcome), not an uncaught runtime error.

SANDBOX-REJECT OK writes to the sentinel file only when:

new_object(MERRY_DATA, source) returns a non-nil compiled script (the source with the forbidden call still COMPILES -- the shadow symbol exists, so compilation succeeds).
run_merry(...) throws (the shadow body raised on first fire).
file_info(HACK_FILE) returns nil (the forbidden write never reached the filesystem).

What the evidence establishes:

The sandbox boundary is enforced at runtime fire, not at compile/registration. A reaction naming a denied kfun binds successfully; the registration step gives no signal that the reaction will fail.
The deny mechanism is implicit-whitelist-by-presence: write_file is denied because a SANDBOX(write_file) shadow masks the real kfun. A kfun is reachable from a Merry script only if no shadow masks it; there is no separate allow list to consult.
The denied operation does not partially occur. The error fires inside the shadow body before any real I/O; hack.txt is never created.
The same load path that runs an in-sandbox reaction to completion (the paired positive Observation) stops a denied reaction at its first fire, with no code-path difference at registration time.

What the evidence does not establish:

Coverage of the full deny list. Only write_file is exercised. The other 50 SANDBOX() entries (plus the explicit call_other / new_object shadows) are asserted to behave identically by the shared macro, but only one is empirically fired here. A sibling example fires clone_object through the same macro, giving a second data point.
Escape attempts past the shadow. The reaction calls the kfun by its bare name and hits the shadow. A probe that tries to reach the real kfun by an aliasing or indirection trick (e.g., constructing the call through a non-shadowed path) and observing it still denied would extend the claim from "bare-name calls are shadowed" to "the shadow cannot be bypassed."
Compile-time rejection of disallowed syntax. The grammar additionally forbids some constructs (e.g., raw -> call_other) at parse time rather than fire time. This Observation exercises the fire-time shadow deny, not the parse-time grammar deny; the two are distinct enforcement layers.
Capability-tier denial. The deny here is the sandbox shadow set, identical across capability tiers. A denial that depends on the loaded code's capability tier (a tier-scoped operation refused for a low tier but permitted for a high one) is a different mechanism not exercised here.

What Would Revise It

A second denied-kfun data point in this example. Exercising a different SANDBOX() entry (e.g., open_port or shutdown) in the chat-app and observing the same compile-succeeds / first-fire-throws shape would extend the claim from single-kfun to the shadow class within this example.
A shadow-bypass probe. A reaction that attempts to reach write_file through an indirection the compiler does not shadow, observing either a denial (boundary holds) or a success (boundary has a hole), would test the completeness of the deny mechanism rather than just its presence.
A deny-list audit against the running binary. A probe that enumerates the DGD 1.7.9 kfun set and cross-checks each escape-shaped kfun against the SANDBOX() list, flagging any escape-shaped kfun NOT shadowed, would convert the implicit-whitelist claim from "the listed kfuns are denied" to "no escape-shaped kfun is reachable." A prior kfun-delta audit at the cohesive-lift landing did a version of this; a runtime re-check would be the empirical counterpart.
A DGD or eOS-kernellib upgrade that adds escape-shaped kfuns or changes the shadow dispatch. The current evidence rests on DGD 1.7.9 plus feature/cohesive-lift HEAD a55b77f. A runtime release adding a new I/O or persistence kfun not yet shadowed, or changing how the Merry compiler resolves a bare call to the local shadow, would invalidate the snapshot claim; the pinning and a per-lift kfun-delta-audit discipline are part of the grounds.

Sources

examples/chat-app/sys/test.c (in eOS-kernellib feature/cohesive-lift) -- phase 4 is the load-bearing sequence: compile the forbidden reaction (separate catch, FAIL on compile-throw), bind it, fire via run_merry expecting a throw, assert the throw fired and no file was created.
src/usr/Merry/lib/merrynode.c (in eOS-kernellib feature/cohesive-lift) -- the SANDBOX(f) macro and the SANDBOX(write_file) entry (line 448). The macro defines a same-named method that unconditionally errors; the Merry compiler resolves the bare write_file call to this method, so compilation succeeds and the error fires at invocation.
src/usr/Merry/lib/merryapi.c (in eOS-kernellib feature/cohesive-lift) -- run_merry calls the compiled script's evaluate, which dispatches the bare call into the merrynode shadow; the boot-log stack passes through merryapi::run_merry line 103.
docs/merry-language.md (in eOS-kernellib feature/cohesive-lift) -- the deny-list reference; documents the 51-entry SANDBOX() list, the explicit call_other / new_object shadows, and that call_out is intentionally NOT sandboxed. States "the sandbox (the runtime layer) is the authoritative deny."
examples/chat-app/README.md -- the verify recipe; expects SANDBOX-REJECT OK and notes the [caught] boot-log error.
docs/chat-applications.md (in eOS-kernellib feature/cohesive-lift) -- the walkthrough; the "Sandboxed reactions" section's Phase 4 quotes the forbidden source and the [caught] error, and explains the implicit-whitelist-by-presence model.
The isolated runtime staging tree's boot log -- carries the [caught] function 'write_file' not allowed in merry code error and the full call stack down to merrynode.c line 448.
The isolated runtime staging tree's src/usr/Chat/data/test-result.log -- the sentinel file; carries SANDBOX-REJECT OK after a clean cold boot.
The instance config and the isolated-runtime materialization used for the smoke.

Relations

conforms_to::[[Observation Form Contract]]
- Carries has_epistemic_status::[[Empirical Observation]], names the measurement (one cold-boot smoke run, phase 4, with the boot-log [caught] stack as corroborating evidence), states the limits (one denied kfun fired; no shadow-bypass probe; fire-time deny not parse-time or tier deny), and lists concrete revision conditions.
informs_downstream::[[Code Load Compiles Into the Live Runtime, Bounded by Capability Tiers]]
- The sandboxed-code-load Conviction's stance is that loaded code runs in the runtime bounded by the platform's enforcement, not by an external sandbox. This Observation is the deny half: a reaction naming a forbidden kfun loads successfully but is stopped at its first fire by the runtime's own shadow set. The paired positive shows the accept side.
informs_downstream::[[Agent Code Containment Stacks Five Axes, Not One]]
- The sandbox kfun-deny is one of the containment axes the Conviction names. This Observation gives empirical evidence for the language-sandbox axis specifically: loaded code's reachable-symbol set is constrained by the shadow list, independent of the other axes (capability tier, file-access mediation, resource limits, atomicity).
grounded_in::[[Conviction Form Contract]]
- The deny is a runtime mechanism, not a policy the loaded code could opt out of. The reaction did not "choose to honor" the deny; it had no resolvable path to the real kfun -- the shadow masks it unconditionally.
contrasts_with::[[A Merry-Compiled Room Reaction Executes Within the Sandbox Surface]]
- The positive-case peer Observation. The two together cover the accept and deny sides of the same load path: the positive shows an in-sandbox reaction compiling and running to completion against room property storage; this case shows a sandbox-denied reaction compiling (registration succeeds) but throwing on first fire. The paired sentinels (SANDBOX-ACCEPT OK and SANDBOX-REJECT OK) land in the same result file across the same cold boot. Reading the deny case alone does not show what successful loaded execution looks like; reading the accept case alone does not show where the boundary is.