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."