From 7fa551d9e4ae08d4cae075bd1b5ef58506c57ee2 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 28 Aug 2026 00:50:33 +0200 Subject: [PATCH] =?UTF-8?q?feature:=20the=20M4-portability=20half=20of=20G?= =?UTF-8?q?I-FPU-002=20is=20RESOLVED=20=E2=80=94=20full=20cascade=20lowers?= =?UTF-8?q?=205/5=20on=20m4f,=20and=20jess's=20obligation=20is=203=20AEABI?= =?UTF-8?q?=20symbols,=20verified=20linkable=20(AFD-046)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The loop asked whether synth#881's "--builtins / M4-portability half" was still unresolved in practice, to be re-filed if so. IT IS RESOLVED. Nothing needs re-filing; it needs jess keeping two promises. The self-contained path still declines 3 functions on m4f, and that is CORRECT — synth refuses to emit f64 on a single-precision FPU (#369). Its own message names the remedy: route the i64<->f32 conversions through the AEABI builtins with --relocatable (#1069). Following that remedy walks a chain of THREE honest-refusal gates, each handing jess an obligation rather than failing quietly: --relocatable -> refuses #1041: 13 active data segments not materialised + --embedder-data-init -> refuses #1052: 12 global initialisers do not reach the object + --embedder-global-init -> exit 0, ZERO skips, 5/5 stages MEASURED (falcon v1.135.0, meld 0.52 --pack-rebase -> loom 1.4.0 -> synth v0.60): cortex-m7dp exit 0 0 skips 5/5 stages 0 external symbols cortex-m4f exit 0 0 skips 5/5 stages 3 external symbols cortex-m3 exit 1 12 skips (soft-float; falcon was never targeted there) JESS'S ENTIRE M4 LINK OBLIGATION IS THREE SYMBOLS: __aeabi_f2lz, __aeabi_l2f, __aeabi_ul2f. m7dp needs NONE — it has the double-precision FPU. "IT LOWERS" IS NOT "IT WORKS", so the obligation was DISCHARGED rather than described: all three are defined in stock arm-none-eabi libgcc (thumb/v7e-m+fp/hard), `arm-none-eabi-ld -r` returns 0 with ZERO undefined remaining, and all 5 stages are still T in the linked object. NEGATIVE CONTROL, asserted by the oracle: linking WITHOUT libgcc leaves exactly those 3 undefined. Without it, "0 undefined" is vacuous — an empty nm is also what a broken object prints. The script FAILS if the negative control comes back empty. A SILENT MISREPORT IN THE ORACLE, CAUGHT BY ITS OWN NEGATIVE CONTROL: the first version used `mapfile`, which does not exist in macOS's bash 3.2, and printed "" for a symbol list that actually had three entries. Step 5 contradicted step 2, which is how it surfaced. Replaced with a portable read, and the script now hard-fails if the list is empty. TWO PROMISES JESS NOW OWES AT INSTANTIATION — real, not paperwork. The flags emit BYTE-IDENTICAL code; they only convert a refusal into an acknowledgement. jess must populate memory 0's active data segments and seed the R9 globals table before any export runs, or every load from the initialised region reads whatever the target memory holds (the gale#278 0xFF class). RELEASE-WATCH, falcon-v1.135.0 — CLEAN, NO REGRESSION: 10/10 digests match, 8/10 pass the publish gate, numerically IDENTICAL to v1.134.1, composed flight-app returns the same 2147484996. A CONTROLLED COMPARISON was run before suspecting a regression: both releases give the same 3 m4f skips under an identical pipeline, so the count is a property of the path, not the release. The two new artifacts (cascade-stream-composed 2.8 MB with wasi:cli, cascade-stream-fused 211 KB core module) are P3 async-STREAM artifacts. They fail C3/C1, which is EXPECTED for host-side artifacts and is NOT reported as a defect. rivet validate PASS. Co-Authored-By: Claude Opus 4.8 --- artifacts/findings.yaml | 59 +++++++++++++++++++++++++++ tools/lowering/_count_exports.sh | 3 ++ tools/lowering/m4-matrix.sh | 68 ++++++++++++++++++++++++++++++++ 3 files changed, 130 insertions(+) create mode 100755 tools/lowering/_count_exports.sh create mode 100755 tools/lowering/m4-matrix.sh diff --git a/artifacts/findings.yaml b/artifacts/findings.yaml index f36e0e7..9edcb10 100644 --- a/artifacts/findings.yaml +++ b/artifacts/findings.yaml @@ -1737,6 +1737,65 @@ artifacts: - type: traces-to target: REQ-PIX-007 + - id: AFD-046 + type: ai-found-defect + severity: major + triage-status: closed + detected-by: jess release-watch on relay falcon-v1.135.0 + per-core lowering matrix, 2026-08-27 + title: THE M4-PORTABILITY HALF OF GI-FPU-002 IS RESOLVED — the FULL 5-stage cascade lowers 5/5 on cortex-m4f via synth's relocatable + embedder-contract path, and jess's obligation is exactly THREE AEABI symbols, verified linkable + status: resolved + description: > + 2026-08-27. The loop asked whether synth#881's "--builtins / M4-portability half" was still + unresolved in practice, to be re-filed if so. IT IS RESOLVED. Nothing needs re-filing; what it + needs is jess keeping two promises. + THE SELF-CONTAINED PATH STILL DECLINES 3 FUNCTIONS ON m4f, AND THAT IS CORRECT BEHAVIOUR, not a + defect: synth refuses to emit f64 on a single-precision FPU (#369). The declined functions are + func_4, position#tick and rate#tick, and synth's own message names the remedy - route the + i64<->f32 conversions through the AEABI builtins with --relocatable (#1069). + FOLLOWING SYNTH'S DOCUMENTED REMEDY WALKS A CHAIN OF THREE HONEST-REFUSAL GATES, each of which + hands jess an obligation rather than failing silently: + --relocatable -> refuses on #1041: 13 active data segments not materialised + + --embedder-data-init -> refuses on #1052: 12 global initialisers do not reach the object + + --embedder-global-init -> exit 0, ZERO skips, 5/5 stages + RESULT, MEASURED (falcon v1.135.0, meld 0.52 --pack-rebase -> loom 1.4.0 -> synth v0.60): + cortex-m7dp exit 0 0 skips 5/5 stages 0 external symbols + cortex-m4f exit 0 0 skips 5/5 stages 3 external symbols + cortex-m3 exit 1 12 skips (soft-float; falcon was never targeted there) + *** JESS'S ENTIRE M4 LINK OBLIGATION IS THREE SYMBOLS ***: __aeabi_f2lz, __aeabi_l2f, + __aeabi_ul2f. m7dp needs NONE - it has the double-precision FPU, so no builtins are required. + "IT LOWERS" IS NOT "IT WORKS", so the obligation was DISCHARGED, not just described: all three + are defined in the stock arm-none-eabi libgcc (thumb/v7e-m+fp/hard multilib), `arm-none-eabi-ld + -r` against it returns 0 with ZERO undefined symbols remaining, and all 5 cascade stages are + still present as T in the linked object. + NEGATIVE CONTROL: linking WITHOUT libgcc leaves exactly those 3 symbols undefined. Without this + the "0 undefined" result would be vacuous - an empty nm is also what a broken object prints. + The oracle asserts the negative control and FAILS if it comes back empty. + TWO PROMISES JESS NOW OWES AT INSTANTIATION, and they are real, not paperwork: the flags emit + BYTE-IDENTICAL code and only convert a refusal into an acknowledgement. jess must (i) populate + memory 0's active data segments and (ii) seed the R9 globals table from the module's + initialisers, before any export runs. If jess does not, every load from the initialised region + and every global.get reads whatever the target memory happens to hold - the gale#278 0xFF class. + RELEASE-WATCH VERDICT ON falcon-v1.135.0 - CLEAN, NO REGRESSION: all 10 published artifacts + match their digests; 8 of 10 pass the publish gate. Numerically IDENTICAL to v1.134.1 (torque + tx=1 ty=0.472507507 tz=-0.147003502 thrust=0.5; the composed flight-app returns the same + 2147484996). A CONTROLLED COMPARISON was run before any regression was suspected: v1.134.1 and + v1.135.0 give the SAME 3 m4f skips under an identical pipeline, so the skip count is a property + of the path, not of the release. + THE TWO NEW ARTIFACTS ARE NOT MCU-TARGETED AND THAT IS FINE: falcon-cascade-stream-composed + (2.8 MB, imports wasi:cli/*) and falcon-cascade-stream-fused (211 KB core module) are P3 + async-STREAM artifacts - stream-new, task-return, stream-cancel-*. They fail jess's publish + gate on C3/C1 respectively, which is expected for host-side artifacts and is NOT reported as a + defect. Worth relay confirming the intended consumer, since P3-async-everywhere is jess's + north star and these are the first shipped P3 artifacts in the stack. + ALSO CONFIRMED: meld#390 reproduces identically with v1.135.0 components, ruling out the falcon + build as a variable; reported on the issue. + tags: [synth, gi-fpu-002, m4f, lowering, aeabi, embedder-contract, release-watch, falcon-v1.135] + links: + - type: traces-to + target: REQ-PIX-021 + - type: traces-to + target: DD-023 + - id: AFD-045 type: ai-found-defect severity: major diff --git a/tools/lowering/_count_exports.sh b/tools/lowering/_count_exports.sh new file mode 100755 index 0000000..c1162dd --- /dev/null +++ b/tools/lowering/_count_exports.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env sh +# Count falcon cascade stages present as defined text symbols in an ARM object. +arm-none-eabi-nm "$1" 2>/dev/null | grep -E ' T ' | grep -cE 'pulseengine:falcon-cascade/[a-z]+@0\.7\.0#' diff --git a/tools/lowering/m4-matrix.sh b/tools/lowering/m4-matrix.sh new file mode 100755 index 0000000..bc1d5b5 --- /dev/null +++ b/tools/lowering/m4-matrix.sh @@ -0,0 +1,68 @@ +#!/usr/bin/env bash +# Lower the FULL 5-stage falcon cascade for cortex-m4f and cortex-m7dp, then LINK the +# m4f object — because "it lowers" is not "it works", and an object with unresolved +# externals is not a shippable image. +# +# WHAT THIS ESTABLISHES (AFD-046): the M4-portability half of GI-FPU-002 is resolved in +# synth v0.60 via the relocatable + embedder-contract path, and jess's obligation as the +# embedder is exactly THREE AEABI symbols, all present in the stock ARM toolchain. +# +# The plain self-contained path still declines 3 functions on m4f — that is NOT a defect, +# it is synth honestly refusing to emit f64 on a single-precision FPU (#369). The fix is +# to route those i64<->f32 conversions through the AEABI builtins, which is what +# --relocatable does, and to accept the two embedder obligations synth then names. +set -uo pipefail +ROOT="$(cd "$(dirname "$0")/../.." && pwd -P)" +OUT="${OUT:-$ROOT/.scratch/m4matrix}"; mkdir -p "$OUT" +SYNTH="${SYNTH:-$ROOT/.scratch/fg60/synth}" +FUSED="${FUSED:?set FUSED to a loom-optimised fused cascade .wasm}" +fail() { printf 'FAIL: %s\n' "$*" >&2; exit 1; } + +[ -x "$SYNTH" ] || fail "synth not found at $SYNTH (campaign uses v0.60; the varve layer carries 0.58)" +command -v arm-none-eabi-nm >/dev/null || fail "arm-none-eabi toolchain not on PATH" + +echo "== 1. lower, declaring the embedder contract ==" +# --embedder-data-init (#1041) jess populates memory 0's active data segments +# --embedder-global-init(#1052) jess seeds the R9 globals table from the module's initialisers +# Neither flag changes a single emitted byte; each converts a REFUSAL into an explicit +# acknowledgement. They are promises jess must actually keep at instantiation. +for core in cortex-m7dp cortex-m4f; do + "$SYNTH" compile "$FUSED" -t $core --cortex-m --relocatable \ + --embedder-data-init --embedder-global-init -o "$OUT/$core.o" >"$OUT/$core.log" 2>&1 \ + || { sed -n 's/^Error: / /p' "$OUT/$core.log" | head -2; fail "$core did not lower"; } + n=$("$ROOT/tools/lowering/_count_exports.sh" "$OUT/$core.o") + echo " $core: exit 0, $n/5 cascade stages exported" + [ "$n" = "5" ] || fail "$core exported $n/5 stages" +done + +echo "== 2. m4f external symbols (the embedder's link obligation) ==" +# NOT `mapfile` — it does not exist in macOS's bash 3.2, and its absence here silently +# printed "" for a symbol list that actually had three entries. +undef="$(arm-none-eabi-nm "$OUT/cortex-m4f.o" | awk '$1=="U"||$2=="U"{print $NF}' | sort -u)" +undef_n=$(printf '%s\n' "$undef" | grep -c . || true) +[ "$undef_n" -gt 0 ] || fail "m4f needs NO external symbols — unexpected; the AEABI route did not engage" +printf '%s\n' "$undef" | sed 's/^/ /' + +echo "== 3. m7dp must need NONE (it has a double-precision FPU) ==" +m7u=$(arm-none-eabi-nm "$OUT/cortex-m7dp.o" | awk '$1=="U"||$2=="U"{print $NF}' | sort -u | wc -l | tr -d ' ') +[ "$m7u" = "0" ] || fail "m7dp unexpectedly needs external symbols ($m7u)" +echo " confirmed: 0 external symbols" + +echo "== 4. LINK m4f against libgcc — proves the obligation is satisfiable ==" +LG=$(arm-none-eabi-gcc -mcpu=cortex-m4 -mfpu=fpv4-sp-d16 -mfloat-abi=hard -print-libgcc-file-name) +arm-none-eabi-ld -r "$OUT/cortex-m4f.o" "$LG" -o "$OUT/m4f.linked.o" || fail "link failed" +left=$(arm-none-eabi-nm "$OUT/m4f.linked.o" | awk '$1=="U"||$2=="U"{print $NF}' | sort -u) +[ -z "$left" ] || fail "still unresolved after linking libgcc: $left" +n=$("$ROOT/tools/lowering/_count_exports.sh" "$OUT/m4f.linked.o") +[ "$n" = "5" ] || fail "linked object lost stages ($n/5) — an empty nm is not a pass" +echo " linked clean, 0 undefined, $n/5 stages still present" + +echo "== 5. NEGATIVE CONTROL: without libgcc the symbols MUST stay undefined ==" +arm-none-eabi-ld -r "$OUT/cortex-m4f.o" -o "$OUT/m4f.nolibgcc.o" 2>/dev/null +nleft=$(arm-none-eabi-nm "$OUT/m4f.nolibgcc.o" | awk '$1=="U"||$2=="U"{print $NF}' | sort -u | wc -l | tr -d ' ') +[ "$nleft" -gt 0 ] || fail "VACUOUS: linking without libgcc left nothing undefined — step 4 proves nothing" +echo " confirmed: $nleft undefined without libgcc, so step 4 was a real resolution" + +echo +echo "PASS — full cascade lowers 5/5 on m7dp AND m4f; m4f's obligation is $undef_n AEABI" +echo " symbol(s), resolved by the stock ARM toolchain, negative-controlled."