From a650ac99b16cd54c4120f314d044c0e7dc648c6f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 7 Sep 2026 16:54:24 +0200 Subject: [PATCH] =?UTF-8?q?feature:=20gale-nano=200.7.0=20EXECUTES=20on=20?= =?UTF-8?q?real=20STM32F100=20silicon=20=E2=80=94=20admit=20works,=20dispa?= =?UTF-8?q?tch=20does=20not=20(AFD-113)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit H3 second half: ADVANCED, NOT COMPLETE. Stated that way deliberately. gale-nano 0.7.0 (digest-pinned) lowered for cortex-m3 and linked against jess's real gust:hal MMIO (AFD-109), the generic embedder-init apply loop (AFD-107) and a boot shim. 4,349 B, 0 undefined, embedder ABI verified. On silicon: 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 exec_state(handle) returns 1, exactly what TEST-PIX-035 asserts. handle 0 is correct, not a failure — jess already recorded that gale-nano hands out handle 0. But exec_poll_round reaches poll-task ZERO times, where the wasmtime reference — re-run green the same day, 8/8, same pinned artifact, same PRIO/DEADLINE/NOW constants taken from app/dispatch-driver — reaches it once. That is a confirmed wasmtime-vs-silicon divergence, which is what jess's lane exists to produce. LIKELY CAUSE, NOT PROVEN, AND NOT A GALE DEFECT. gale-nano's component manifest declares exactly two imports (gust:os/taskdisp, gust:hal/mmio) and exports gust:os/{time,log,spawn,exec,timer} — matching gale#223 in words. But `synth --relocatable --all-exports` emits SIX undefined symbols and an export set that does not match the declared one: it emits gust:sched/tasks@0.1.0#*, which the component does NOT export, and nothing for gust:os/time@0.1.0, which it DOES. Nothing in the object separates the 2 real obligations from the 4 internals, and 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 does. - `deadline` has nothing to alias to, because the gust:os/time export was not lowered. Returning 0 broke 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. Two harness defects of jess's own, both caught by the reference rather than by inspection: - the first run used deadline=(0,0), now=(0,0); the reference's own comment says NOW must be PAST the deadline for a task to be READY. Reporting that as "gale-nano does not dispatch on silicon" would have been a false supplier report — the meld#390 shape. - the openocd readback filter `^0x2000048` silently dropped the exec_state word at 0x20000490 — the one reading that localises the fault. Co-Authored-By: Claude Opus 4.8 --- artifacts/findings.yaml | 75 ++++++++++++ hardware/silicon/f100-gale-nano/README.md | 92 +++++++++++++++ hardware/silicon/f100-gale-nano/boot.S | 92 +++++++++++++++ hardware/silicon/f100-gale-nano/build.sh | 110 ++++++++++++++++++ .../silicon/f100-gale-nano/gust_os_embed.S | 72 ++++++++++++ hardware/silicon/f100-gale-nano/link.ld | 12 ++ .../silicon/f100-gale-nano/run-on-silicon.sh | 71 +++++++++++ 7 files changed, 524 insertions(+) create mode 100644 hardware/silicon/f100-gale-nano/README.md create mode 100644 hardware/silicon/f100-gale-nano/boot.S create mode 100755 hardware/silicon/f100-gale-nano/build.sh create mode 100644 hardware/silicon/f100-gale-nano/gust_os_embed.S create mode 100644 hardware/silicon/f100-gale-nano/link.ld create mode 100755 hardware/silicon/f100-gale-nano/run-on-silicon.sh diff --git a/artifacts/findings.yaml b/artifacts/findings.yaml index 6d7f227..10d3785 100644 --- 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 . 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 new file mode 100644 index 0000000..db29017 --- /dev/null +++ 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 new file mode 100644 index 0000000..e0348ca --- /dev/null +++ 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 diff --git a/hardware/silicon/f100-gale-nano/build.sh b/hardware/silicon/f100-gale-nano/build.sh new file mode 100755 index 0000000..9388218 --- /dev/null +++ b/hardware/silicon/f100-gale-nano/build.sh @@ -0,0 +1,110 @@ +#!/usr/bin/env bash +# Link gale-nano 0.7.0 for the STM32F100 and gate the result (H3 second half). +# +# gale-nano (PINNED oci artifact) -> synth --relocatable --embedder-data-init +# --embedder-global-init -t cortex-m3 +# + jess's REAL gust:hal read32/write32 (AFD-109) +# + jess's generic embedder-init apply loop (AFD-107) +# + gust_os_embed.S — jess's HARNESS for the gust:os seam, not an implementation +set -uo pipefail +D="$(cd "$(dirname "$0")" && pwd)" +ROOT="$(cd "$D/../../.." && pwd -P)" +OUT="${OUT:-$ROOT/.scratch/f100gale}"; mkdir -p "$OUT" +SYNTH="${SYNTH:?set SYNTH to a synth binary}" +PY="${PY:-python3}" +GALE="${GALE:-$ROOT/.scratch/galenano7/gale-nano-0.7.0.wasm}" +fail() { printf 'FAIL: %s\n' "$*" >&2; exit 1; } +command -v arm-none-eabi-gcc >/dev/null || fail "arm-none-eabi-gcc not on PATH" +[ -f "$GALE" ] || fail "gale-nano artifact not found: $GALE" + +# The artifact must be the PINNED one. A differential against an unpinned gale-nano is a +# result about whatever happened to be in .scratch. +want=546531952a5cf0edb05ea804bb77dea9ec2786530cef8310bd718559eeede86f +got=$(shasum -a 256 "$GALE" 2>/dev/null | awk '{print $1}') +[ -z "$got" ] && got=$(sha256sum "$GALE" | awk '{print $1}') +[ "$got" = "$want" ] || fail "gale-nano is not the pinned artifact + want $want + got $got" +echo "gale-nano: pinned artifact verified ($want)" + +"$SYNTH" compile "$GALE" -t cortex-m3 --cortex-m --relocatable --all-exports \ + --embedder-data-init --embedder-global-init -o "$OUT/gale.o" >"$OUT/lower.log" 2>&1 \ + || { tail -3 "$OUT/lower.log"; fail "gale-nano did not lower for cortex-m3"; } +# Wire gale-nano's intra-component imports to its OWN exports. See gust_os_embed.S. +# Renaming is the only route: the export names contain `@`, which begins an ARM comment, +# so they cannot be referenced from a .S label at all. +arm-none-eabi-objcopy \ + --redefine-sym 'gust:sched/tasks@0.1.0#set-deadline=set-deadline' \ + --redefine-sym 'gust:sched/tasks@0.1.0#slept-status=slept-status' \ + --redefine-sym 'gust:sched/tasks@0.1.0#state=state' \ + "$OUT/gale.o" "$OUT/gale.aliased.o" || fail "objcopy --redefine-sym failed" +for s in set-deadline slept-status state; do + arm-none-eabi-nm "$OUT/gale.aliased.o" | grep -qE "^[0-9a-f]+ T $s\$" \ + || fail "'$s' is not DEFINED after aliasing — gale-nano's own export did not get renamed" +done +mv "$OUT/gale.aliased.o" "$OUT/gale.o" +echo "sched imports aliased to gale-nano's own exports (3)" + +n=$(grep -ci 'skip' "$OUT/lower.log" || true) +[ "$n" = "0" ] || { cat "$OUT/lower.log"; fail "$n skip line(s) — the image is incomplete"; } + +# The gust:os seam must BE a seam. If these stopped being undefined, gale-nano would be +# calling something other than jess's harness and the differential would measure nothing. +for s in poll-task deadline read32; do + arm-none-eabi-nm "$OUT/gale.o" | grep -qE "^ +U $s\$" \ + || fail "'$s' is not undefined in the lowered object — the embedder seam is absent" +done +echo "embedder seam present: poll-task, deadline, read32 (the 3 jess genuinely owes)" + +"$PY" "$ROOT/tools/embedder-init/extract_init.py" "$GALE" \ + --out-c "$OUT/init_tables.c" --out-manifest "$OUT/init.json" >"$OUT/einit.log" 2>&1 \ + || { cat "$OUT/einit.log"; fail "init extraction failed"; } +segs=$($PY -c "import json;print(len(json.load(open('$OUT/init.json'))['segments']))") +globs=$($PY -c "import json;print(len(json.load(open('$OUT/init.json'))['globals']))") +[ "$segs" -gt 0 ] && [ "$globs" -gt 0 ] || fail "empty init tables — a vacuous instantiation" +echo "init tables: $segs segment(s), $globs global(s)" + +# The image must FIT the real part: linear memory base 0x20000600 + 0x1000 must stay under +# 0x20002000, and every declared segment must land inside it. AFD-088 is why this is checked +# rather than assumed — an emulator sized to the artifact hid a 6-week-old misfit. +top=$($PY -c "import json;d=json.load(open('$OUT/init.json'));print(max((s['offset']+s['len']) for s in d['segments']))") +[ "$top" -le 4096 ] || fail "highest data address $top exceeds the 4096 B linear-memory window" +echo "geometry: highest data address $top B <= 4096 B window (real 8 KB part)" + +CPU="-mcpu=cortex-m3 -mthumb" +arm-none-eabi-gcc -c $CPU -ffreestanding -O2 "$OUT/init_tables.c" -o "$OUT/tables.o" || fail "tables did not compile" +arm-none-eabi-gcc -c $CPU -ffreestanding -O2 -ffixed-r9 -ffixed-r10 -ffixed-r11 \ + "$ROOT/hardware/silicon/f100-init/apply_init.c" -o "$OUT/apply.o" || fail "apply loop did not compile" +arm-none-eabi-gcc -c $CPU -ffreestanding -O2 -ffixed-r9 -ffixed-r10 -ffixed-r11 \ + "$ROOT/hardware/silicon/f100-gust-hal/gust_hal.c" -o "$OUT/hal.o" || fail "gust_hal did not compile" +arm-none-eabi-gcc -c $CPU "$D/gust_os_embed.S" -o "$OUT/embed.o" || fail "embedder harness did not assemble" +arm-none-eabi-gcc -c $CPU "$D/boot.S" -o "$OUT/boot.o" || fail "boot.S did not assemble" + +LG="$(arm-none-eabi-gcc $CPU -print-libgcc-file-name)" +arm-none-eabi-ld -T "$D/link.ld" -o "$OUT/f100gale.elf" \ + "$OUT/boot.o" "$OUT/gale.o" "$OUT/embed.o" "$OUT/hal.o" "$OUT/apply.o" "$OUT/tables.o" "$LG" \ + || fail "link failed" + +left="$(arm-none-eabi-nm "$OUT/f100gale.elf" | awk '$1=="U"||$2=="U"{print $NF}' | sort -u)" +[ -z "$left" ] || fail "undefined after linking: $left" +nsym=$(arm-none-eabi-nm "$OUT/f100gale.elf" | wc -l | tr -d ' ') +[ "$nsym" -gt 0 ] || fail "no symbols in the linked image — the check above would be vacuous" +ram=$(arm-none-eabi-readelf -S "$OUT/f100gale.elf" | grep -E '\.data|\.bss') +[ -z "$ram" ] || fail "image has RAM sections nothing initialises: $ram" + +if [ -n "${SYNTH_VERIFY:-}" ]; then + command -v "$SYNTH_VERIFY" >/dev/null 2>&1 || [ -x "$SYNTH_VERIFY" ] \ + || fail "SYNTH_VERIFY='$SYNTH_VERIFY' is not an executable — 'could not run', not 'failed'" + "$SYNTH_VERIFY" verify-embedder --allow-writer reset "$OUT/f100gale.elf" >"$OUT/ve.log" 2>&1 \ + || { cat "$OUT/ve.log"; fail "embedder ABI violated across gale-nano + harness"; } + "$SYNTH_VERIFY" verify-embedder "$OUT/f100gale.elf" >/dev/null 2>&1 \ + && fail "verify-embedder ACCEPTED the image unacknowledged — it can no longer refuse" + echo "embedder ABI: OK (writes confined to ; refusal still works)" +elif [ -n "${REQUIRE_VERIFY:-}" ]; then + fail "REQUIRE_VERIFY set but SYNTH_VERIFY is not" +else + echo "embedder ABI: NOT CHECKED (set SYNTH_VERIFY to a synth >= 0.62)" +fi + +arm-none-eabi-objcopy -O binary "$OUT/f100gale.elf" "$OUT/f100gale.bin" || fail "objcopy" +echo "built $OUT/f100gale.elf ($(wc -c <"$OUT/f100gale.bin") B raw, $nsym symbols)" diff --git a/hardware/silicon/f100-gale-nano/gust_os_embed.S b/hardware/silicon/f100-gale-nano/gust_os_embed.S new file mode 100644 index 0000000..a207610 --- /dev/null +++ b/hardware/silicon/f100-gale-nano/gust_os_embed.S @@ -0,0 +1,72 @@ + .syntax unified + .cpu cortex-m3 + .thumb +@ jess's EMBEDDER HARNESS for the gust:os seam — NOT an implementation of gust:os. +@ +@ gale owns gust:os semantics (DD-025, gale#223/#224 are still open on the timer). +@ These exist so gale-nano's lowered code can be EXECUTED on real silicon and the +@ dispatch seam observed. They are the on-target counterpart of app/gust-dispatch-probe, +@ which plays the same role for the wasmtime oracle (TEST-PIX-035). +@ +@ WRITTEN IN ASSEMBLY ON PURPOSE, for two reasons: +@ 1. The import names are WIT kebab-case (`poll-task`, `set-deadline`, ...). GCC cannot +@ declare them: `__asm__("poll-task")` emits an unquoted `.type poll-task, %function` +@ and the assembler rejects it. A quoted label in .S does work. +@ 2. It makes the calling convention unfalsifiable. `deadline` is `func(u64, u64) -> u64` +@ and the core flattening of u64 is not something to guess: a wrong C prototype +@ silently corrupts registers. A leaf that sets its return registers and returns is +@ correct for ANY argument shape, because under AAPCS the CALLER cleans the stack. +@ They also must not touch r9/r10/r11 — synth's embedder contract — which is trivially +@ true here and is checked by verify-embedder over the linked image. + + .equ POLL_COUNT, 0x20000484 @ must match boot.S + + .text + +@ poll-task(id: u32) -> u32 +@ COUNTS its invocations. A stub that returns a value and records nothing makes +@ "poll-round drained the task" and "poll-round did nothing" observationally +@ IDENTICAL — the exact vacuity tools/dispatch/run.sh was written to avoid, in its +@ own words: "jess's existing taskdisp implementations returned 0 and recorded +@ NOTHING". The counter is what makes the control pair mean anything. + .global "poll-task" + .thumb_func +"poll-task": + ldr r1, =POLL_COUNT + ldr r2, [r1] + adds r2, r2, #1 + str r2, [r1] + movs r0, #1 @ 1 = complete. Polarity MEASURED in AFD-067: returning 0 + bx lr @ leaves the task ready and it is re-polled every round. + +@ time.deadline(now: u64, ticks: u64) -> u64 = now + ticks +@ +@ NOTE THIS IS A JESS GUESS AT A GALE SEMANTIC, and it is here only to isolate one +@ variable. gale-nano's component manifest EXPORTS gust:os/time@0.1.0 — this is NOT an +@ embedder import (its only two are taskdisp and mmio) — but synth's --relocatable +@ lowering emits no symbol for that export and leaves `deadline` dangling, so there is +@ nothing to alias to. Returning 0 was MEASURED to break dispatch on silicon: admit +@ succeeded (exec_state == 1) and poll-round never reached poll-task. +@ u64 args flatten to (lo,hi) pairs in r0..r3; a u64 result returns in r0:r1. + .global "deadline" + .thumb_func +"deadline": + adds r0, r0, r2 + adcs r1, r1, r3 + bx lr + +@ gust:sched/tasks {set-deadline, slept-status, state} are NOT stubbed here. +@ +@ gale-nano DEFINES them (as `gust:sched/tasks@0.1.0#...`) and ALSO imports them by bare +@ name: synth's --relocatable lowering does not wire a component's intra-component imports +@ to its own exports, so they arrive as undefined symbols and look like an embedder +@ obligation. They are not. In the wasmtime graph wac infers exactly this wiring (see +@ tools/dispatch/compose.wac, which names only taskdisp and mmio and leaves `...` to +@ inference). +@ +@ Stubbing them was measured to be WRONG, not merely redundant: with inert stubs returning +@ 0, exec_admit returned handle 0 and poll-round never reached poll-task on silicon — +@ jess had replaced gale's task-state store with a no-op. build.sh now aliases gale's own +@ exports onto the imported names with objcopy --redefine-sym (the same technique +@ cascade-invoke already uses, because `@` begins an ARM comment and an asm label +@ truncates there). diff --git a/hardware/silicon/f100-gale-nano/link.ld b/hardware/silicon/f100-gale-nano/link.ld new file mode 100644 index 0000000..6dc80c7 --- /dev/null +++ b/hardware/silicon/f100-gale-nano/link.ld @@ -0,0 +1,12 @@ +/* .rodata is its OWN output section, never folded into .text (AFD-105: folding + mapped 43,005 B of wasm data EXECUTABLE and synth's verify-embedder caught it). */ +MEMORY { + FLASH (rx) : ORIGIN = 0x08000000, LENGTH = 128K + RAM (rwx) : ORIGIN = 0x20000000, LENGTH = 8K +} +SECTIONS { + .vectors : { KEEP(*(.vectors)) } > FLASH + .text : { *(.text*) } > FLASH + .rodata : { *(.rodata*) } > FLASH + /DISCARD/ : { *(.ARM.exidx*) *(.comment) } +} diff --git a/hardware/silicon/f100-gale-nano/run-on-silicon.sh b/hardware/silicon/f100-gale-nano/run-on-silicon.sh new file mode 100755 index 0000000..d41b1d0 --- /dev/null +++ b/hardware/silicon/f100-gale-nano/run-on-silicon.sh @@ -0,0 +1,71 @@ +#!/usr/bin/env bash +# H3 second half: gale-nano 0.7.0's dispatch loop EXECUTING on real STM32F100 silicon. +# +# Both legs run the BYTE-IDENTICAL flashed image and differ in exactly ONE word — ADMIT +# at 0x20000480, written by this host before `resume`. With a task admitted, poll-round +# must reach jess's `poll-task`; without one it must not. Same control pair as the +# wasmtime oracle TEST-PIX-035, which is what makes this a DIFFERENTIAL rather than a +# fresh assertion. +set -uo pipefail + +WD="${WITH_DEVICE:-$HOME/bench/with-device}" +if [ -z "${WD_REENTRY:-}" ] && [ -x "$WD" ]; then + export WD_REENTRY=1 + exec "$WD" stlink-v1 --purpose "gale-nano dispatch loop on F100 silicon" -- "$0" "$@" +fi + +OOCD="sudo -n openocd -f interface/stlink-hla.cfg -f target/stm32f1x.cfg" +ADMIT=0x20000480; COUNT=0x20000484; RES_H=0x20000488; DONE=0x2000048C; RES_ST=0x20000490 + +BACKUP="${BACKUP:-$HOME/bench/f100-backup/original-flash.bin}" +BACKUP_SHA=10969f5c35de715696c377c2ae367b9be5950698115f3f91adf479bb12a0a78b +if [ -z "${SKIP_BACKUP_CHECK:-}" ]; then + [ -f "$BACKUP" ] || { echo "REFUSING TO WRITE: no recovery image at $BACKUP" >&2; exit 2; } + got=$(sha256sum "$BACKUP" | awk '{print $1}') + [ "$got" = "$BACKUP_SHA" ] || { echo "REFUSING TO WRITE: recovery hash mismatch" >&2; exit 2; } + echo "recovery image verified" +fi + +BIN="${BIN:-$HOME/bench/f100gale.bin}" +[ -f "$BIN" ] || { echo "missing image: $BIN"; exit 2; } +echo "image: $BIN ($(wc -c <"$BIN") B)" + +echo "=== flash at 0x08000000 ===" +$OOCD -c "init; halt" -c "flash write_image erase $BIN 0x08000000" \ + -c "verify_image $BIN 0x08000000" -c "shutdown" 2>&1 | grep -iE "wrote|verified|error" | head -4 + +run_leg() { + $OOCD -c "init" -c "reset halt" -c "mww $ADMIT $1" \ + -c "resume" -c "sleep 300" -c "halt" \ + -c "mdw $COUNT 1" -c "mdw $RES_H 1" -c "mdw $DONE 1" -c "mdw $RES_ST 1" \ + -c "shutdown" 2>&1 | grep -E "^0x200004" # NOT ^0x2000048 — that silently drops 0x20000490 +} + +echo +printf "%-42s %-11s %-9s %-9s %s\n" "LEG (only the ADMIT word differs)" "poll-task#" "handle" "state" "completion" +rc=0 +for leg in "1|task admitted (baseline)|ge1" "0|no admit (negative control)|eq0"; do + IFS='|' read -r flag label want <}" "$h" "${st:-}" "$d" "$ok" +done +echo +[ $rc -eq 0 ] && echo "PASS — gale-nano's dispatch loop ran on silicon and reached the embedder only when a task was admitted." || echo "FAIL" +exit $rc