pulseengine · avrabe · Aug 27, 2026 · Aug 27, 2026
diff --git 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
@@ -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
@@ -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 "<none>" 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."