pulseengine · avrabe · Sep 7, 2026 · Sep 7, 2026
diff --git a/artifacts/findings.yaml b/artifacts/findings.yaml
@@ -6330,3 +6330,78 @@ artifacts:
       detected-by: assessing varve v0.32.1 and varve-core 0.32.1 against jess's four consumer asks, 2026-09-07
       severity: major
       triage-status: confirmed
+
+  - id: AFD-113
+    type: ai-found-defect
+    title: "gale-nano 0.7.0 EXECUTES on real STM32F100 silicon and admit works (gale's own exec_state==1, matching wasmtime) but poll-round does NOT dispatch — and synth's --relocatable component lowering emits 6 undefined symbols where the component declares only 2 imports"
+    status: open
+    description: |-
+      2026-09-07. H3 second half: ADVANCED, NOT COMPLETE. Stated that way on purpose.
+
+      *** WHAT EXECUTED ON SILICON (STM32VLDISCOVERY, ST-LINK/V1, fourpi bench) ***
+      gale-nano 0.7.0 (digest-pinned 546531952a5c...) lowered for cortex-m3, linked against
+      jess's real gust:hal MMIO (AFD-109), jess's generic embedder-init apply loop (AFD-107) and
+      a boot shim; 4,349 B image, 0 undefined, embedder ABI verified.
+          LEG (only the ADMIT word differs)   poll-task#  handle    state     completion
+            task admitted (baseline)          00000000    00000000  00000001  c0ffee00
+            no admit (negative control)       00000000    deadbeef  deadbeef  c0ffee00
+      GALE'S CODE RUNS ON THE PART, and exec_admit WORKS: gale's OWN view, exec_state(handle),
+      returns 1 — exactly what TEST-PIX-035 asserts ("admitted task starts in state 1").
+      handle == 0 is CORRECT, not a failure: jess already recorded that gale-nano hands out
+      handle 0 (app/gust-dispatch-probe's WIT says so, which is why its never-called sentinel is
+      0xFFFFFFFF).
+
+      *** THE DIVERGENCE ***
+      exec_poll_round reaches poll-task ZERO times on silicon. The wasmtime reference was re-run
+      GREEN the same day against the same pinned artifact (exit 0, 8/8 assertions) and reaches it
+      ONCE: `with-admit() 1`, `without-admit() 0`, `state-before-round() 1`. Both sides use the
+      SAME constants (PRIO=1, DEADLINE_LO=1000, NOW_LO=2000) taken from app/dispatch-driver.
+      This is the on-target differential doing its job — the thing jess's lane exists for.
+
+      *** THE LIKELY CAUSE, NOT PROVEN, AND NOT A GALE DEFECT ***
+      gale-nano's COMPONENT manifest (wasm-tools component wit) declares exactly two imports —
+      gust:os/taskdisp and gust:hal/mmio — and exports gust:os/{time,log,spawn,exec,timer}. That
+      matches gale#223 in words: the embedder IMPLEMENTS {mmio, taskdisp} and CALLS the rest.
+      But `synth --relocatable --all-exports` emits SIX undefined symbols —
+      deadline, poll-task, read32, set-deadline, slept-status, state — and an export set that does
+      not match the declared one: it emits `gust:sched/tasks@0.1.0#*`, an interface the component
+      does NOT export, and emits NOTHING for `gust:os/time@0.1.0`, which it DOES.
+      Nothing in the object distinguishes the 2 real obligations from the 4 component internals.
+      Satisfying them the obvious way is MEASURABLY wrong:
+        - stubbing set-deadline/slept-status/state inert replaced gale's task-state store. Aliasing
+          them onto gale's OWN exports via objcopy --redefine-sym is correct and is what build.sh
+          now does (`@` begins an ARM comment, so an .S label cannot name them — the same
+          constraint cascade-invoke already works around).
+        - `deadline` has NOTHING to alias to, because the gust:os/time export was not lowered.
+          Returning 0 was measured to break dispatch; a `now + ticks` guess did not fix it either.
+      jess is NOT going to keep guessing at a gale semantic — that is gale's lane, and inventing
+      one is how a stub becomes a false claim.
+
+      *** WHAT IS NOT CLAIMED ***
+      Not a gale defect: gale-nano's component is self-consistent and the wasmtime path is green.
+      Not a proven synth defect either, until synth confirms the export/import asymmetry is
+      unintended — filed with the measurement rather than a diagnosis.
+      NOT claimed: that H3's second half is done. gale-nano executes; it does not dispatch.
+
+      *** WHY THE CONTROL IS NOT VACUOUS ***
+      Byte-identical flashed image both legs, one host-written word differs. poll-task COUNTS its
+      invocations (a recording-nothing stub makes "drained" and "did nothing" identical — the
+      vacuity tools/dispatch/run.sh names in its own header). POLL_COUNT is a counter so it cannot
+      be poisoned, which makes the completion marker load-bearing; it is present in BOTH legs, so
+      "0 invocations" is distinguished from "the CPU never ran". And exec_state is read back so the
+      positive half rests on GALE'S own view, not only jess's counter — that is what localises the
+      failure to poll-round rather than to admit.
+
+      *** TWO HARNESS DEFECTS OF JESS'S OWN, FOUND BY THE REFERENCE ***
+      (a) The first silicon run used deadline=(0,0) and now=(0,0). The reference's own comment says
+          NOW must be PAST the deadline for a task to be READY. Reporting that first result as
+          "gale-nano does not dispatch on silicon" would have been a false report against a
+          supplier — the meld#390 shape, avoided by driving both sides identically.
+      (b) The openocd readback filter was `grep -E "^0x2000048"`, which silently dropped the
+          exec_state word at 0x20000490 and reported it as <none>. A harness that drops the one
+          reading that localises the fault.
+    tags: [gale-nano, on-target, silicon, stm32f100, h3, synth, differential, wasmtime, partial]
+    fields:
+      detected-by: running gale-nano 0.7.0's dispatch loop on F100 silicon against the wasmtime reference, 2026-09-07
+      severity: major
+      triage-status: confirmed
diff --git a/hardware/silicon/f100-gale-nano/README.md b/hardware/silicon/f100-gale-nano/README.md
@@ -0,0 +1,92 @@
+# gale-nano 0.7.0 on real STM32F100 silicon — H3's second half, ADVANCED not COMPLETE
+
+## What executed
+
+gale-nano 0.7.0 (digest-pinned, `546531952a5c…`) lowered for `cortex-m3` and linked against
+jess's embedder — the real `gust:hal` MMIO from AFD-109, the generic embedder-init apply loop
+from AFD-107, and a boot shim — then flashed to an STM32VLDISCOVERY and run over SWD.
+
+```
+LEG (only the ADMIT word differs)   poll-task#  handle    state     completion
+  task admitted (baseline)          00000000    00000000  00000001  c0ffee00
+  no admit (negative control)       00000000    deadbeef  deadbeef  c0ffee00
+```
+
+**gale-nano's code runs on the part.** `exec_admit` works and gale's *own* view agrees with
+the wasmtime reference: `exec_state(handle) == 1`, which is exactly what TEST-PIX-035 asserts
+("admitted task starts in state 1"). `handle == 0` is correct, not a failure — jess already
+recorded that gale-nano hands out handle 0.
+
+**`exec_poll_round` does not dispatch.** `poll-task` is reached **0** times. The wasmtime
+reference, re-run green the same day against the same pinned artifact, reaches it **once**:
+
+```
+with-admit()          1   a round after admit polls the task ONCE
+without-admit()       0   CONTROL: same round, no admit -> poll-task NOT reached
+state-before-round()  1   admitted task starts in state 1
+```
+
+Both sides use the same constants (`PRIO=1`, `DEADLINE_LO=1000`, `NOW_LO=2000`) — taken from
+`app/dispatch-driver`, not invented here.
+
+## The likely cause, and why it is not yet proven
+
+gale-nano's **component manifest** declares:
+
+```
+import gust:os/taskdisp@0.1.0;
+import gust:hal/mmio@0.1.0;
+export gust:os/time@0.1.0;  export gust:os/log@0.1.0;  export gust:os/spawn@0.1.0;
+export gust:os/exec@0.1.0;  export gust:os/timer@0.1.0;
+```
+
+So the embedder owes exactly **two** things — `poll-task` and `read32`/`write32` — which is
+what gale#223 says in words.
+
+But `synth --relocatable --all-exports` emits **six** undefined symbols:
+
+```
+deadline  poll-task  read32  set-deadline  slept-status  state
+```
+
+and the emitted export set does not match the declared one: it emits
+`gust:sched/tasks@0.1.0#*` (an interface the component does **not** export) and emits
+**nothing** for `gust:os/time@0.1.0` (which it **does**).
+
+Nothing in the object distinguishes the two real obligations from the four that are the
+component's own internals. Satisfying them the obvious way is measurably wrong:
+
+- **Stubbing** `set-deadline`/`slept-status`/`state` inert replaced gale's task-state store.
+  Aliasing them onto gale's own exports with `objcopy --redefine-sym` is correct and is what
+  `build.sh` does. (`@` begins an ARM comment, so an `.S` label cannot name these; this is the
+  same technique `cascade-invoke` already uses.)
+- `deadline` has **nothing to alias to**, because the `gust:os/time` export was not lowered.
+  Returning `0` was measured to break dispatch; a `now + ticks` guess did not fix it either.
+  jess is not going to keep guessing at a gale semantic — that is gale's lane.
+
+**Not claimed:** that this is a gale defect. gale-nano's component is self-consistent and the
+wasmtime path works. The asymmetry is in the lowering, and the remaining gap is unproven.
+
+## Why the control is not vacuous
+
+- Both legs run the **byte-identical flashed image**; one host-written word at `0x20000480`
+  differs. Exactly one variable.
+- `poll-task` **counts** its invocations. A stub that returns a value and records nothing makes
+  "poll-round drained the task" and "poll-round did nothing" identical readings — the vacuity
+  `tools/dispatch/run.sh` was written to avoid, in its own words.
+- `POLL_COUNT` is a counter, so it cannot be poisoned; the **completion marker** is therefore
+  load-bearing, and it is present in **both** legs. "0 invocations" is distinguished from "the
+  CPU never ran".
+- `exec_state` is read back so the result rests on **gale's own view**, not only jess's counter.
+  That is what proves admit succeeded and localises the failure to `poll-round`.
+
+## Scope
+
+- **Executed on silicon:** gale-nano's lowered code, `exec_admit`, `exec_state`,
+  `exec_poll_round`, and jess's `read32` linked in.
+- **Not achieved:** dispatch. H3's second half is **not** complete.
+- Nothing on the RT1176; the debug adapter is in transit.
+
+`build.sh` verifies the pinned digest before lowering, asserts the seam is exactly the three
+symbols jess supplies, checks the 11 data segments fit the 4 KB window on the real 8 KB part,
+and gates on `verify-embedder` plus its refusal control.
diff --git a/hardware/silicon/f100-gale-nano/boot.S b/hardware/silicon/f100-gale-nano/boot.S
@@ -0,0 +1,92 @@
+    .syntax unified
+    .cpu cortex-m3
+    .thumb
+@ Run gale-nano 0.7.0's dispatch loop on real STM32F100 silicon (H3, second half).
+@
+@ SRAM map (the REAL part: 8 KB at 0x20000000):
+@   0x20000000..0x20000400  stack (SP = 0x20000400)
+@   0x20000480  ADMIT      <- written by the HOST before resume; the ONE variable
+@   0x20000484  POLL_COUNT    incremented by the `poll-task` embedder stub
+@   0x20000488  admit handle returned by exec_admit
+@   0x2000048C  completion marker (0xC0FFEE00)
+@   0x20000500  globals table (R9), 10 globals
+@   0x20000600  linear memory (R11), 0x1000 B  (gale-nano's highest data addr is 0xC11)
+    .equ SP_TOP,    0x20000400
+    .equ ADMIT,     0x20000480
+    .equ POLL_COUNT,0x20000484
+    .equ RES_H,     0x20000488
+    .equ RES_ST,    0x20000490      @ exec_state(handle) — gale's OWN view
+    .equ DONE,      0x2000048C
+    .equ GLOBALS,   0x20000500
+    .equ LINMEM,    0x20000600
+    .equ LINMEM_SZ, 0x1000
+
+    .section .vectors, "a"
+    .word SP_TOP
+    .word reset + 1
+
+    .text
+    .global reset
+    .thumb_func
+reset:
+    ldr  sp, =SP_TOP
+@ POLL_COUNT must start at 0 — it is a counter, not a sentinel, so it cannot be
+@ poisoned. That makes "0 invocations" and "the program never ran" the same reading,
+@ which is why the completion marker below is load-bearing rather than decorative:
+@ it is the only thing that separates them.
+    movs r0, #0
+    ldr  r1, =POLL_COUNT
+    str  r0, [r1]
+    ldr  r1, =0xDEADBEEF
+    ldr  r0, =RES_H
+    str  r1, [r0]
+    ldr  r0, =RES_ST
+    str  r1, [r0]
+    ldr  r0, =DONE
+    str  r1, [r0]
+
+@ Apply the 11 active data segments and seed the 10 R9 globals BEFORE any export runs
+@ (AFD-107). Called first because the C helper is free to clobber r9/r10/r11.
+    ldr  r0, =LINMEM
+    ldr  r1, =GLOBALS
+    bl   jess_wasm_apply_init
+
+    ldr  r9,  =GLOBALS
+    ldr  r10, =LINMEM_SZ
+    ldr  r11, =LINMEM
+
+@ exec_admit(prio, deadline_lo, deadline_hi) -> handle
+    ldr  r0, =ADMIT
+    ldr  r0, [r0]
+    cmp  r0, #0
+    beq  1f
+@ THE SAME CONSTANTS AS THE WASMTIME REFERENCE (app/dispatch-driver), not invented here.
+@ A first run used deadline=(0,0) and now=(0,0); admit returned handle 0 and poll-round
+@ never reached poll-task. That is not a lowering defect and not a gale defect — the
+@ reference's own comment says why: NOW must be PAST the deadline for an admitted task to
+@ be READY. Reporting that first result as "gale-nano does not dispatch on silicon" would
+@ have been a false report against a supplier (the meld#390 shape). The differential is
+@ only a differential if both sides are driven identically.
+    movs r0, #1                 @ prio           = PRIO
+    movw r1, #1000              @ deadline_lo    = DEADLINE_LO
+    movs r2, #0                 @ deadline_hi    = DEADLINE_HI
+    bl   exec_admit
+    ldr  r1, =RES_H
+    str  r0, [r1]
+@ Ask gale for ITS view of the task, independent of jess's counter. The wasmtime oracle
+@ asserts "admitted task starts in state 1"; if silicon reports something else, admit did
+@ not take, and the poll-count is a downstream symptom rather than the finding.
+    bl   exec_state
+    ldr  r1, =RES_ST
+    str  r0, [r1]
+1:
+@ exec_poll_round(now_lo, now_hi) — drives one round. With a task admitted this must
+@ reach `poll-task`; without one it must not. That is the whole differential.
+    movw r0, #2000              @ now_lo = NOW_LO (past the deadline -> task is READY)
+    movs r1, #0                 @ now_hi = NOW_HI
+    bl   exec_poll_round
+
+    ldr  r0, =0xC0FFEE00
+    ldr  r1, =DONE
+    str  r0, [r1]
+2:  b    2b