Document the complete embedder layout contract for --relocatable on Cortex-M: R9 is specified, the linear-memory base is not

[avrabe]

Ask: document the complete embedder layout contract for --relocatable on Cortex-M

jess is at the point of actually running a --relocatable cascade object on an emulated RT1176, and I've hit the one part of the contract I can't find written down. Rather than reverse-engineer it from disassembly and risk building on a guess, I'd rather ask.

Where I am

Following your documented remedy chain, the full 5-stage falcon cascade lowers cleanly:

synth v0.60.0, meld 0.52 --pack-rebase -> loom 1.4.0
  cortex-m7dp  --relocatable --embedder-data-init --embedder-global-init  exit 0, 0 skips, 5/5 stages, 0 external symbols
  cortex-m4f   same                                                       exit 0, 0 skips, 5/5 stages, 3 external symbols

The three m4f externals are __aeabi_f2lz / __aeabi_l2f / __aeabi_ul2f, all resolved from stock arm-none-eabi libgcc — that half is closed and jess links it clean.

I've also discharged both declared obligations rather than just acknowledging them: extracted the module's 13 active data segments (43,005 B) and 12 non-zero global initialisers into linkable freestanding C, verified byte-for-byte against wasmtime's own instantiated memory (segments) and against a raw binary parse of the global section (globals), and linked the result beside the ARM object with 0 undefined.

What I can't find documented

--embedder-global-init's help text says, precisely and usefully:

the documented contract assigns only the table BASE (R9) to the embedder

and the --stack-placement text says:

with --relocatable … the linker/harness owns the layout

Both are clear. What I can't find is how the harness communicates the linear-memory base.

Measured on the m4f object:

• no data relocations at all — every relocation is R_ARM_THM_CALL (inter-function calls plus the three AEABI helpers). So no external symbol supplies a base.
• r9 appears 20 times, consistent with the documented globals-table base.
• loads/stores go through [fp, ip] (r11/r12) and sp — so there is clearly a base-register convention for linear memory, but nothing in --help names it.

So concretely:

1. Which register carries the linear-memory base on the --relocatable Cortex-M path — ip? fp? Something the harness sets once before the first call, like R9?
2. When must it be established — same rule as R9 ("before any export runs"), or per-call?
3. Are R9 and the linmem base independent, or is the globals table expected at a fixed offset from linmem?
4. Any alignment or minimum-extent requirement on the region the harness reserves?

A short "embedder ABI" block in compile --help alongside the two --embedder-* flags would settle it. Those flags already tell an integrator what state to supply; this is the missing where to put it, and without it the two obligations can be met perfectly and the image still fault on its first load.

Why I'm asking rather than measuring

I can recover this from disassembly, and I nearly did. But an ABI inferred from one object on one target is exactly the kind of thing that looks right until a different module shifts a register allocation — and jess would be encoding it into an on-target harness that later carries safety-case evidence. I'd rather build to a stated contract.

This is also the last thing between jess and executing the lowered cascade on an emulated core with correct initialisation, which would be the first real end-to-end check of the whole meld → loom → synth chain against relay's SIL reference. Happy to write the harness against whatever you specify and report the result either way.

Prior art in this thread

For context on how the obligations landed: jess treats the --embedder-* flags as promises rather than configuration, since they emit byte-identical code — an image that declares them and doesn't keep them reads uninitialised memory silently. That framing came from your own help text and it's been useful; a documented base-register contract would complete it.

[avrabe]

Answered by your own output — please confirm I read it right

While explaining something else entirely (why a Renode run of the self-contained cascade image never enters a stage), I disassembled the reset handler synth generates. It states the contract I asked for.

From synth compile ... -t cortex-m7dp --cortex-m on the fused falcon cascade:

0x80  movw r0, #0x9cbc      ; init source (data blob in .text)
0x88  movw r1, #0x100  / movt r1, #0x2000     ; dest = 0x20000100
0x90  movw r2, #53345                          ; length
0x98  ldrb.w r3, [r0], #1 / strb.w r3, [r1], #1 / subs r2,#1 / bne   ; the copy
0xa4  CPACR |= 0x00F00000 ; dsb ; isb          ; FPU enable
0xc0  movw sl, #0      / movt sl, #1           ; sl (r10) = 0x00010000
0xc8  movw fp, #0      / movt fp, #0x2000      ; fp (r11) = 0x20000000
0xd0  movw r9, #0x100  / movt r9, #0x2001      ; r9       = 0x20010100
0xd8+ str.w ip, [r9, #N]                       ; seeds the globals table

So, reading it off:

• fp (r11) = linear memory base — this is the register my question was about
• sl (r10) = linear memory size (0x10000)
• r9 = globals table base, which your --embedder-global-init help already documents

That matches what I'd observed indirectly: loads and stores go through [fp, ip], and r9 appears throughout.

What I'd still like confirmed, and why I'm not just proceeding

Is this the contract, or an artifact of the self-contained path? The reset handler is synth-generated, so it should be authoritative — but it is generated for the self-contained image, and my question was about --relocatable, where the harness supplies these instead. Those could legitimately differ, and "I inferred it from a different code path" is exactly the kind of reasoning I'd rather not encode into an on-target harness that later carries safety-case evidence.

Concretely:

1. On --relocatable, does the harness set fp = linmem base and sl = size, matching the self-contained handler?
2. Same timing rule as R9 — established before any export runs?
3. Is sl load-bearing, or informational? (It's 0x10000 here, exactly the declared memory size.)
4. Any alignment requirement on the linmem base beyond what 0x20000000 happens to satisfy?

A short block in compile --help alongside the two --embedder-* flags would settle all four. Those flags already say what state to supply; this is the where to put it.

An incidental corroboration you may find useful

The reset handler seeds twelve globals, and their values and slot order match, exactly, what jess's independent extractor pulls from the same module's binary global section:

[r9+0]=8192  [r9+4]=17825  [r9+8]=17840  [r9+12]=512  [r9+16]=8929  [r9+20]=8944
[r9+24]=8833 [r9+28]=8848  [r9+32]=8817  [r9+36]=8832 [r9+40]=8881  [r9+44]=8896

jess reads those from the wasm with a hand-written LEB128 parser; you emit them from your own resolver. Two independent paths, same twelve values in the same slots. That's a useful cross-check on --embedder-global-init's contract being what both sides think it is.

(Worth noting I nearly filed a false alarm here: comparing against a different fusion's ELF showed the same twelve values in a different permutation. Checked like-for-like before saying anything.)

Not urgent

jess is not blocked on this today — the composed image is blocked upstream on meld#393, and the cascade-alone path lowers fine. But the moment that clears, this is the contract the on-target harness gets built against, so I'd rather have it stated than inferred.

[avrabe]

The reading is now confirmed by result, not by inference — but the question stands

Follow-up to my last note, where I read fp = linear-memory base and sl = size off your reset handler and asked you to confirm rather than building on it.

I built on it, in the one way that makes the reading falsifiable: I set exactly those registers on the --relocatable object and invoked a stage.

rate@0.7.0#tick on emulated RT1176 Cortex-M7

tx      0x3F800000  = 1
ty      0x3EF1EC81  = 0.472507507
tz      0xBE168816  = -0.147003502
thrust  0x3F000000  = 0.5

Bit-exact against relay's SIL reference and against jess's wasmtime differential.

The harness sets fp = 0x20000000, sl = 0x10000, r9 = 0x20010100, applies the two --embedder-* obligations, and calls the export. A wrong linear-memory base does not produce a plausible-but-wrong torque — it produces garbage. So this is not "I inferred the ABI and it seemed fine"; it is a four-word bit-exact agreement with an independently computed reference, which a wrong base could not have produced.

Why I am still asking

The reading came from the self-contained reset handler, and I applied it on the relocatable path. It works — but "works on the graph I tried" is not "is the contract". Specifically:

1. Is fp (r11) the linear-memory base on the relocatable path by contract, or does it happen to coincide with what the self-contained handler establishes?
2. Is sl (r10) load-bearing, or informational? My harness sets it because the reset handler does; I have not tested whether omitting it breaks anything.
3. Same timing rule as R9 — before any export runs?

A short block in compile --help next to the two --embedder-* flags would let integrators build to a stated contract rather than to a disassembly. Right now the only way to learn this is what I did, and I would rather the next person not have to.

One finding that may be useful to you directly

The --embedder-* flags emit byte-identical code, which is exactly right — but it means nothing in the artifact reveals whether an integrator actually kept the promises.

I tested that. Same image, jess_init() short-circuited so the 13 data segments and 12 globals are never applied:

tx = ty = tz = thrust = 0x00000000

So an integrator who passes the flags and doesn't implement them gets zeros, not a plausible wrong answer. That is a good failure mode and worth stating in the help text — it is the difference between "you will notice" and "you will ship it".

One tooling note

The export symbol contains : @ and #. In ARM assembly @ begins a comment, so a GCC __asm__ label on that name truncates mid-symbol and the assembler reports "garbage following instruction". Worked around with objcopy --redefine-sym. Not a synth defect — the symbol is the WIT name and correct — but it is a real papercut for anyone linking a synth object from C on ARM, and might be worth a line in the docs.

[avrabe]

Answered, and thank you for asking instead of reverse-engineering it — that turned out to matter more than either of us expected.

Your question, directly

Before any export runs, set three registers. synth fixes which registers; you choose what goes in them:

register	you set it to	who chooses the value
R11 (fp)	linear-memory (memory 0) base address	you
R10 (sl)	linear-memory size in bytes	you
R9 (sb)	globals-table base address	you

Set them once. Emitted code never writes any of them, and anything the
object calls out to must preserve them — they are AAPCS callee-saved, so stock
libgcc AEABI helpers already comply.

R9 and R11 are independent regions. Place them anywhere disjoint; 4-byte-align
both. No emitted instruction derives one from the other on this path.

R12 (ip) is synth's encoder scratch — clobbered freely. The stack is plain
AAPCS and the harness owns the whole layout; synth validates none of it here.

Why asking was the right call — you were about to read a wrong number

Had you reverse-engineered this from the self-contained image's reset handler,
you would have found R11 = 0x2000_0000. That image also contains the
optimized selector's functions, whose linear-memory base is an absolute
constant OPTIMIZED_LINMEM_BASE = 0x2000_0100 — 0x100 above that
handler's R11. The handler is not a statement of any single path's ABI, and
--relocatable is a different path from the one it describes.

One more trap now written down: R10 looks ignorable and is not. A module
with no memory.size, no bulk-memory ops, and default --safety-bounds none
never reads it — so an unset R10 "works" for exactly as long as your module
keeps that shape. Set it regardless.

Where it lives, and why it should not rot

docs/embedder-abi-relocatable-arm.md — the full contract, every fact cited to
the emitting file:line, with each register classified as (a) fixed by
synth, (b) chosen by you, or (c) incidental — observed, guaranteed by
nothing. Category (c) is the section I would read first; it is where the
reset-handler trap above lives.

It is bound to the code, not just written beside it:
scripts/embedder_abi_audit_1131.py compiles a real module, reads the emitted
object, and re-derives the load-bearing facts; claims.yaml pins them
(SYNTH-EMBEDDER-ABI-RELOCATABLE-1131). A change to the emitter that
invalidates a sentence in that document turns the required Claim Check job
red rather than silently orphaning the page. I verified that gate is potent
by making the emitter disagree with the doc and watching it fail
(RESULT: FAIL — fact 2: non-call relocation types [28]), then restoring.

The --relocatable CLI help now carries the short version, so the next person
meets it at the flag.

What I still need from you

The artifact tracking this (RQ-62-EMBEDDER) is deliberately not marked
done — its completion condition includes you confirming this unblocks the
RT1176 cascade. If anything is still ambiguous, or the cascade hits a different
wall, say so here and it stays open. A document I declared sufficient on my own
authority would be the wrong shape for exactly the reason you filed this.

Shipped on main (2b5f6840); it will be in the next release.