The mismatch is reachable from flan reload, and the guard does not close it

HANDOFF-x86-aggregates.md

@@ -4,46 +4,156 @@ Branch `dev-loop`, from `957ba07`. This closes item 4 of `HANDOFF-x86-redef.md`:
 takes and returns a struct, which is the one case the two backends' conventions disagree about and the reason
 `X86.redefinition` exists at all rather than reusing `Emit.redefinition`.
 
-*Status: in progress. This file is written early and on purpose, so that a lane that picks the work up mid-way
+**The claim is now measured and it holds.** An `--x86` host dlopening `--x86` modules gets the right answer
-has the plan and not just the diff.*
+when four redefined functions each take a struct and return one. The same fixture, built and reloaded entirely
+through LLVM, prints the same transcript. And the crossed pair — an `--x86` host given LLVM-built modules —
+dies with SIGSEGV on the first such call, which is the measurement the "same-convention-by-construction"
+argument was standing in for.
 
-## The plan
+## What was built
 
-1. A fixture pair, `test/programs/reload-agg.flan` and `reload-agg-v2.flan`, beside the existing `reload.flan`
+| file | what |
-   rather than inside it — `reload.flan`'s transcript is shared with the LLVM path and must not move.
-   No `main`; the host is `test/reload_host.c` unchanged, which wants `outer : () -> i64` and a `counter`
-   global. Everything aggregate happens *inside* Flan, between the host's compiled-once call site and the
-   redefined body, because the C boundary is where the two conventions are required to agree and is not what
-   is under test.
-2. Four struct shapes, because SysV treats them in four different ways and `x86.ml` treats all four the same:
-   - `≤16 bytes, all integer` — SysV passes in `rdi`:`rsi` and returns in `rax`:`rdx`; `x86.ml` passes a
-     pointer and returns through a hidden `sret`. Diverges in both directions.
-   - `>16 bytes` — SysV copies the argument onto the stack, which `x86.ml` does not; the *return*, though,
-     is a hidden pointer in the first integer register for SysV too, so that half may well coincide. Worth
-     knowing, and worth not assuming either way.
-   - `{f64, f64}` — SysV classifies both eightbytes SSE and uses `xmm0`:`xmm1`.
-   - `{i64, f64}` — one INTEGER and one SSE eightbyte, so `rax` and `xmm0`, which is a third register pattern
-     again.
-3. Every field weighted by position in the printed answer (`a + 100*b + 10000*c + …`), so that a scrambled
-   field order, a wrong base pointer or a half-loaded eightbyte prints a visibly wrong integer rather than the
-   right one by symmetry. A test whose answer is a symmetric sum of the fields passes under a convention
-   mismatch that merely permutes them.
-4. Run it on both backends: the LLVM `Emit.redefinition` path as the control, and the `X86.redefinition` path
-   as the claim. The same transcript from both is the measurement.
-
-## Open questions recorded rather than asked
-
-- Whether the MEMORY-return half of the matrix genuinely coincides between the two conventions, or only looks
-  as though it should. Measured by the mismatch spike rather than argued.
-
-## Baseline
-
-| | before |
 |---|---|
-| `spike/x86/survey.sh` | 99 MATCH / 0 DIFFER / 0 refused |
+| `test/programs/reload-agg.flan` | the fixture. No `main`, so `test/reload_host.c` is the host, unchanged |
-| `spike/x86/cells.sh` | 4/4 ok |
+| `test/programs/reload-agg-v2.flan` | the same four signatures with different arithmetic |
-| `dune test --root .` | exit 0 |
+| `test/test_reload.ml` | the aggregate section, run on both backends against one transcript, plus the two refusal checks |
+| `lib/build.ml` — `shared`, `shared_x86` | a symmetric refusal when the option record names the other backend. Two `failwith`s and their comments; nothing else in the file moved |
 
-Note in advance: `survey.sh` globs `test/programs/*.flan`, so each new no-`main` fixture adds one to its
+Nothing in `lib/x86.ml` was touched.
-`no-main` skip count. That number moving is the fixtures existing and is not a regression; the MATCH count is
+
-what must not move.
+## The fixture, and why it is shaped this way
+
+Everything aggregate happens *inside* Flan, between the host's compiled-once call site and the redefined body.
+The C boundary stays scalar on purpose: that is where the two conventions are required to agree, `check.ml`
+already refuses an aggregate in a `declare` signature, and it is not what is under test. `outer` returns `i64`
+and `counter` is `i64`, so `reload_host.c` needed no change at all.
+
+Four struct shapes, because SysV treats them four different ways and `x86.ml` treats all four the same:
+
+- `Pair` — two INTEGER eightbytes; SysV passes in `rdi`:`rsi` and returns in `rax`:`rdx`.
+- `Quad` — thirty-two bytes, so MEMORY.
+- `Duo` — two SSE eightbytes, `xmm0`:`xmm1`.
+- `Mix` — one INTEGER and one SSE.
+
+Each of the four redefined `step-*` takes its struct and returns it, so a single call crosses the boundary in
+both directions. Each calls a `weigh-*` the module does *not* define, which hands an aggregate the other way —
+module to host — and doubles as the tripwire `reload.flan`'s `helper` is: v2's text for all four `weigh`
+functions multiplies by ten, and since a module declares a sibling rather than defining it, that text has to be
+dead. A module that grew its own copy would print 12411 where the expected transcript says 1611.
+
+Every field is weighted by position in the answer (`a + 100b + 10000c + 1000000d`) rather than summed. A
+symmetric sum would print the right number under a convention mismatch that merely permuted the fields, which
+is the way a test like this passes while proving nothing.
+
+The `defstruct` blocks are byte-identical between the two files and must stay that way. Layout is computed per
+module, so a field reordered in v2 would make host and module disagree about offsets — a real bug, but one
+wearing this test's clothes and indistinguishable in the transcript from the thing the fixture is for.
+
+The arithmetic in the test is derived in a comment rather than read off a run, and both backends are held to
+the same string. The LLVM row is not decoration: a wrong expected number would otherwise be indistinguishable
+from a backend that is right, and two independently-built agreements on one transcript are what rule that out.
+
+## The transcript
+
+```
+a1
+host 54063108
+a1
+after1 54063108
+a2
+after2 104337044
+counter 12
+```
+
+Identical from `Emit.redefinition` + `Build.shared` and from `X86.redefinition` + `Build.shared_x86`.
+`counter` is stepped from inside the redefined body — by one in v1, by ten in v2 — so 1 + 1 + 10 = 12 is the
+host's global written by three different bodies in turn.
+
+## The mismatch, measured
+
+The same run crossed: an `--x86` host, LLVM-built modules.
+
+```
+FAIL  cross aggregate reload
+        got: "a1\nhost 54063108\na1\n" (exit 139)
+     wanted: "a1\nhost 54063108\na1\nafter1 54063108\na2\nafter2 104337044\ncounter 12\n"
+```
+
+Exit 139 is SIGSEGV. It dies on the first call into a redefined aggregate body, before `after1` is printed.
+
+Note what this does and does not say. It says the crossed pair is fatal. It does **not** give a per-shape
+breakdown: `step-pair` is called first and kills the process, so `step-quad`, `step-duo` and `step-mix` never
+run under the crossed pair at all. Whether the MEMORY-return half of the matrix happens to coincide between the
+two conventions is still unmeasured, and would need four crossed runs isolating one `step` at a time. Nothing
+in this lane needs the answer; the four shapes earn their place as *all four cross correctly on a matched
+pair*, which is what was asked for.
+
+This case is not in `dune test`. It is undefined behaviour, and what it prints is a property of whichever LLVM
+is installed; a test that pinned it would be pinning the shape of a crash.
+
+## The serious finding: nothing refuses a mismatched pair, and the CLI can build one
+
+There is no check anywhere that a redefinition module was built by the same backend as its host.
+`Build.shared` and `Build.shared_x86` are unrelated functions, neither looked at `opts.x86`, and the loaded
+object carries no mark saying which backend made it.
+
+**It is reachable from the CLI, by a user doing nothing unusual.** `bin/main.ml:441` reads `--x86` for
+`flan build` only. `flan reload` (`bin/main.ml:506`–523) hardcodes `Build.shared` with
+`{ default with dev = true; debug }` and has no `--x86` spelling at all. So:
+
+```
+flan build game.flan --x86 --dev -o game     # an --x86 host, with cells
+flan reload game.flan changed.flan -o v2.so  # an LLVM module, silently
+```
+
+and the agent in `vendor/agent/flan_agent.c` dlopens `v2.so` into that host. If any redefined function in
+`changed.flan` takes or returns a struct, that is the exit-139 above, at a call site, in a running game, with
+nothing anywhere having said a word.
+
+### What was done about it
+
+`Build.shared` now refuses an option record with `x86` set, and `Build.shared_x86` refuses one without it, each
+naming the reason. Both refusals are asserted in `test/test_reload.ml`.
+
+**That guard does not close the hole, and it was re-measured after landing to be sure.** The crossed run above
+passes both refusals — it hands `Build.shared` an honest LLVM option record and simply loads the result into an
+x86 host — and it still segfaults. The guard catches a caller holding *one* option record and reaching for the
+wrong builder, which is the accident a lane wiring item 3 would make. It cannot catch a caller holding two, and
+`flan reload` is exactly that caller.
+
+### The recommended complete fix, not done here
+
+A marker symbol. `X86.program` defines `flan.abi.x86` and `X86.redefinition` emits an undefined reference to
+it; `Emit.program` defines `flan.abi.llvm` and `Emit.redefinition` references that. A crossed pair then fails
+at `dlopen` with an undefined-symbol message naming the ABI, before a single instruction of the new body runs —
+the loader refusing the pair rather than the processor refusing it at a call. It costs one symbol in each of
+four functions and nothing at run time.
+
+It was not done here because it needs edits in `lib/x86.ml`, which two other lanes are in, and because a
+refusal at the wrong moment is worse than a loud one slightly later. It should be done next, together with item
+3 of `HANDOFF-x86-redef.md` — when `flan dev` and `flan reload` learn to choose host and module backend
+together, the marker is what makes the choice checkable rather than merely intended.
+
+## Baseline, before and after
+
+| | before | after |
+|---|---|---|
+| `spike/x86/survey.sh` | 99 MATCH / 0 DIFFER / 0 REFUSED / 0 NOX86 | **99 / 0 / 0 / 0** |
+| skip breakdown | 28 does-not-compile / 6 no-main / 2 runs-forever | 28 / **8** / 2 |
+| `spike/x86/cells.sh` | 4/4 ok | **4/4 ok** |
+| `dune test --root .` | exit 0 | **exit 0** |
+
+The `no-main` count moving from 6 to 8 is the two new fixtures existing: `survey.sh` globs
+`test/programs/*.flan`, and a program with no `main` fails the LLVM link and is classified there, before the
+x86 build is attempted. The MATCH count is what must not move, and it did not.
+
+One thing to know if you re-run the survey to check this: the shell expands that glob once, when the loop
+starts. A survey launched before the fixtures were written will report 6 and look like a contradiction.
+
+## What remains
+
+- The marker symbol above, and item 3 of `HANDOFF-x86-redef.md` with it.
+- A per-shape crossed measurement, if anyone ever wants to know *which* of the four disagree and how. Four runs
+  isolating one `step` at a time. Nothing depends on it.
+- Items 1, 2 and 5 of `HANDOFF-x86-redef.md`, untouched: the new-name path, the transient thunk, and items 2–7
+  of `HANDOFF-x86-rt.md` §6.

lib/build.ml

@@ -887,12 +887,16 @@ let shared ?(opts = default) ~ir ~out () : timing =
      option record is where the backend choice lives, so a builder handed the
      other backend's record refuses by name rather than producing that object.
 
-     This is a guard and not a proof: a caller holding two option records can
+     Be clear about how little this catches, because a guard that reads wider
-     still pick the wrong one, and the loaded object carries no mark saying
+     than it is is worse than none. It catches a caller holding one option
-     which backend made it. The complete answer is a marker symbol the host
+     record and reaching for the wrong builder. It does not catch a caller
-     defines and a module references, so the loader refuses the pair at dlopen
+     holding two and picking the wrong one — the crossed pair that was measured
-     rather than the processor refusing it at a call. See
+     segfaulting passes this check and still segfaults, because it hands an
-     HANDOFF-x86-aggregates.md. *)
+     LLVM record to the LLVM builder and simply loads the result into an x86
+     host. [flan reload] is precisely that caller. The complete answer is a
+     marker symbol the host defines and a module references, so the loader
+     refuses the pair at dlopen rather than the processor refusing it at a
+     call. See HANDOFF-x86-aggregates.md. *)
   if opts.x86 then
     failwith
       "--x86: Build.shared is the LLVM redefinition path, and an --x86 host \

test/test_reload.ml

@@ -355,17 +355,16 @@ let () =
 
        That is not asserted here. It is undefined behaviour and what it prints
        is a property of whichever LLVM is installed; a test that pins it would
-       be pinning the shape of a crash. What is asserted is that the two
+       be pinning the shape of a crash.
-       builders refuse to be crossed when the option record says which backend
-       is in play — see below. *)
 
-    (* Which is the only thing that stands between a future caller and that
+       What is asserted is narrower, and the gap between the two is the finding
-       segfault. [Build.opts] is where the backend choice lives, so a builder
+       rather than a caveat on it: [Build.opts] is where the backend choice
-       handed an option record belonging to the other backend refuses rather
+       lives, so a builder handed the *other* backend's option record refuses.
-       than producing an object that links, loads, and then dies at a call
+       The crossed run above passes both refusals — it hands [Build.shared] an
-       site. It is not a complete defence and must not be read as one: a caller
+       LLVM record and never calls [Build.shared_x86] at all — and it still
-       that keeps two option records and picks the wrong one by hand defeats
+       segfaults with this guard in place, re-measured after it landed. The
-       it, and the CLI can still do exactly that — see
+       guard catches a caller holding one option record; it cannot catch a
+       caller holding two, and [flan reload] is exactly that caller. See
        HANDOFF-x86-aggregates.md. *)
     (match Build.shared ~opts:x86 ~ir:"" ~out:(tmp "never.so") () with
      | _ -> fail "Build.shared accepted an --x86 option record"