The handoff says what was built, and the index knows it is there

docs/README.md

@@ -55,9 +55,11 @@ built the redefinition emitter, `handoffs/HANDOFF-x86-aggregates.md` took that a
 information, and `handoffs/HANDOFF-x86-cost.md` measured what the backend costs and set the survey running on its
 own so a refusal cannot sit unnoticed again.
 
-The other four sessions are unrelated to each other. `handoffs/HANDOFF-arith.md` is why a divide by zero is a condition
+The other six sessions are unrelated to each other. `handoffs/HANDOFF-arith.md` is why a divide by zero is a condition
 rather than a `SIGFPE`. `handoffs/HANDOFF-raylib-ports.md` is the running record of the last two raylib example
-ports, whose lasting findings were folded into `PORTING.md`. `handoffs/HANDOFF-devtest-noise.md` is the linker
+ports, whose lasting findings were folded into `PORTING.md`, and `handoffs/HANDOFF-cimport-ptr.md` is the arm
+`cimport.ml`'s header check had been promising in a comment and not implementing — which is what those two ports
+found, worked around and wrote up. `handoffs/HANDOFF-devtest-noise.md` is the linker
 error `dune test` used to print on every run. `handoffs/HANDOFF-emacs-flake.md` is the `test_emacs` flake that
 turned out to be `SIGPIPE` killing the daemon mid-reply, and it is worth reading for the two mechanisms it
 rules out as much as for the one it found. `handoffs/HANDOFF-tidy.md` is this reorganisation.

docs/handoffs/HANDOFF-cimport-ptr.md

@@ -1,47 +1,132 @@
 # Handoff — the pointer arm `agrees` already promised
 
 `lib/cimport.ml`'s `agrees` decides whether a hand-written `declare-c` and the C header
-say the same thing. Its comment has always listed three differences that are "expected and
-are not reported"; the code implements two of them. The missing one — *a `(Ptr T)` where
+say the same thing. Its comment had always listed three differences that are "expected and
+are not reported"; the code implemented two of them. The missing one — *a `(Ptr T)` where
 the header says `T *`* — is what `../PORTING.md` §A.1 and §A.2 ran into, and it is why
-`GetCodepointPrevious` cannot be bound honestly and why `UpdateTexture` has to be handed
+`GetCodepointPrevious` could not be bound honestly and why `UpdateTexture` had to be handed
 `(addr (.r (at (slice-from-ptr pixels n) 0)))`.
 
-This file is the running record of building that arm.
+The arm is built. This file is the record of what it accepts, what it still refuses, and
+the one thing that turned out not to be its fault.
 
-## The plan
+## What the arm is
 
-1. A `ptr_agrees` beside `agrees`, consulted only at the two `declare-c` sites in
-   `diff_bound`, where the C spelling is still in hand. `agrees` itself is left alone:
-   `check_structs` uses it for field *widths*, and loosening it there is the hazard the
-   check exists to catch.
-2. Breadth, decided rather than fallen into — see "What it accepts" below.
-3. Rewrite the comment at `lib/cimport.ml:1291` so it describes the code instead of
-   promising it, and take the rotting binding count out of it.
-4. Use it: `get-codepoint-previous-raw` in `vendor/raylib/raylib.flan`, and the
-   `(Ptr Color)` binding for `UpdateTexture`. Delete both workarounds.
-5. `docs/PORTING.md` §A.1 and §A.2 annotated closed in the file's existing style.
+`ptr_agrees` and `agrees_c` beside `agrees` in `lib/cimport.ml`, consulted only from the
+two `declare-c` sites in `diff_bound`. It takes the **C spelling** and not only the
+rendered Flan type, because by the time a parameter has been rendered the header's word is
+gone: `param_ty` turns `const char *` into `string` and `value_ty` turns `void *` into
+`(Ptr u8)`, and neither of those is what the header said. A hand-written line that
+disagrees with a rendering is not disagreeing with the header, and that distinction is the
+whole of the arm.
 
-## What it accepts (to be confirmed as it is built)
+`agrees` itself is untouched. `check_structs` uses it for field **widths**, and a struct
+field is about layout — every pointer in a struct is one word whatever it points at — so
+widening it there would buy nothing and would cost the discipline the field check exists
+to keep.
+
+## What it accepts
 
 - `(Ptr T)` against a C `T *` for the same `T`.
-- `(Ptr u8)` against `char *` — a byte is a byte, and the two spellings of one are not a
-  width disagreement. Scoped to the pointee, never to `agrees` at large.
-- `(Ptr T)` for any `T` against `void *`. `value_ty` already *invents* `(Ptr u8)` for a
-  `void *`, so the check as it stands enforces cimport's own guess as if the header had
-  said it.
-- `const` does not enter into it, because a non-const `char *` parameter makes `param_ty`
-  refuse and `diff_bound` skips a parameter it cannot render at all.
+- `(Ptr u8)` against `char *` and `const char *`. Inside a pointer, `char` and
+  `unsigned char` are two spellings of one byte and the package uses `(Ptr u8)` for both.
+  The `i8`/`u8` tolerance is the **pointee's** and not the world's; as a scalar or a field
+  the two are still a real disagreement, and there is a test for that.
+- `(Ptr T)` for **any** `T` against `void *` and `const void *`. This is the judgement
+  call and the reason is sharper than "it is opaque": `value_ty` *invents* the `(Ptr u8)`
+  it renders a `void *` as, so the check without this arm was enforcing cimport's own guess
+  as if the header had said it. What is **not** given up is that it is a pointer at all —
+  the Flan side must still be a `(Ptr _)`, so an `i32` or a `string` declared against a
+  `void *` is still a finding. raylib spells thirty-odd parameters `void *` and none of
+  them is a scalar.
+- `(Ptr Key)` against a header's `int *`, through the existing enum arm. The same four
+  bytes through a pointer as beside one.
 
-## What it still refuses
+## What it refuses
 
-- `(Ptr A)` against `B *` for different named `A` and `B`.
-- Anything that is not a pointer on the Flan side against a C pointer, and the reverse.
+- `(Ptr A)` against `B *` for different named `A` and `B`. Two structs of the same size
+  are still two different structs.
+- Anything that is not a pointer on the Flan side against a C pointer, `void *` included.
+- Everything `agrees` already refused, unchanged.
 
-## Status
+## What `const` does here: nothing, and the reason is invisible
 
-- [ ] the arm
-- [ ] the comment
-- [ ] tests, positive and negative
-- [ ] the two raylib bindings
-- [ ] PORTING.md
+Worth writing down because reading the code does not show it. A non-const `char *`
+parameter makes `param_ty` **refuse**, and `diff_bound`'s `| None -> None` means a
+parameter the importer cannot render at all is *skipped rather than compared*. So a
+hand-written `(Ptr u8)` over a `char *` has always passed — unexamined, not approved. Only
+`const char *` ever reaches the comparison, and that is the case the arm exists for. The
+rewritten comment at the head of `diff_bound` now says so.
+
+## The comment at `lib/cimport.ml:1291`
+
+Rewritten from a promise into a description. The count it carried — "176 `declare-c`
+lines", against a real 196 — is gone rather than corrected, and the comment says why a
+census written beside a growing file is not a thing to maintain. `vendor/raylib/headers`
+carried the same rot ("425 declarations … 172 hand-written", really 463 and 196) and got
+the same treatment.
+
+## Then it was used
+
+**§A.1 came out entirely, and it is the arm's own case.**
+`vendor/raylib/raylib.flan` has `get-codepoint-previous-raw` — `(Ptr u8)` over a
+`const char *`, which is precisely what the arm was missing — and a `get-codepoint-previous`
+wrapper that takes the bytes and an offset and builds the interior pointer itself.
+`generated.flan` no longer carries the `string`-faced version: a binding that is wrong for
+the only direction it reads in is worse than no binding, and the hand-written declaration
+suppresses the generated one by C symbol. `examples/text-codepoints-loading.flan`'s
+`step-back` is one call to it; the continuation-byte walk and `continuation?` are deleted.
+The answer is 12356 and 3, verified by running it.
+
+`test/programs/raylib-codepoints.flan` would have caught the old answer, verified by
+perturbation rather than by argument: make `step-back` set `size` to 0 — which is exactly
+what the broken string call produced — and both rows go red, because the backward walk
+never reaches offset 0 and runs off the end of its array.
+
+**§A.2's call site came out; the cast moved rather than vanished.** The header check does
+accept the `(Ptr Color)` binding now. What the header check was masking is that
+`lib/shim.ml:651` refuses a second `declare-c` for a C symbol the package already binds,
+and that rule is right: a shim emits one C prototype per declaration, and two prototypes
+for `UpdateTexture` that disagree about a parameter type is a C file that does not compile.
+Its message says what to write instead — "another Flan name for it is a defn" — so
+`raylib.flan` has `update-texture-colors`, a one-line defn over the generated
+`update-texture`:
+
+```flan
+(defn update-texture-colors [texture Texture2D  pixels (Ptr Color)] ()
+  (update-texture texture (addr (.r pixels))))
+```
+
+The `(Ptr u8)` face has to stay the declared one, because `(.data im-copy)` is already a
+`(Ptr u8)` over the same bytes and `(Ptr u8)` → `(Ptr Color)` is the direction the language
+cannot write. `(addr (.r pixels))` was checked against the bytes rather than reasoned
+about: a `gen-image-color 2 1 red` through `load-image-colors`, read back through the `u8`
+pointer, gives 230 41 55 255. So the honest statement is that §A.2 is half closed — the
+example reads `(rl/update-texture-colors texture pixels)`, the cast exists once with a name
+and a comment on it instead of once per call site, and the general gap the section is
+actually about is a **pointer reinterpretation**, which is not a checker arm.
+
+## Verification
+
+- `dune build --root .` and `dune test --root .` clean; the dev suite is 232 checks, 0
+  failures, unchanged — the new checks are in `test_flan.ml`, which reports pass/fail
+  rather than a count.
+- Eleven new checks in `test/test_flan.ml` over three new functions in
+  `test/headers/sample.h` (`blit`, `scratch`, `pair_len_p`): six that must agree, five
+  that must still be reported, each asserting on the message and not on a count. All
+  eleven were confirmed live by breaking `ptr_agrees` in three different directions and
+  watching the right subset go red.
+- The raylib acceptance cases ran rather than skipped (`ldconfig` finds
+  `libraylib.so.550`); the only "skipping" line in the whole run is the web one, which
+  wants a wasm build of raylib that is not in this tree.
+- `flan generate-c vendor/raylib` completes, which is itself the check: it compares every
+  `defstruct`, every hand-written `declare-c` and every mapped constant against
+  `raylib-5.5.h` and refuses to write when they disagree.
+- `bash web/examples/check.sh` green.
+- `spike/x86/survey.sh` at 103 MATCH / 0 DIFFER / 0 REFUSED.
+
+## Still open
+
+- A pointer reinterpretation in the language. `(addr (.r p))` works when the first field
+  is the type you want and there is no general form of it. This is §A.2's real subject.
+- Nothing else. The three differences the comment lists are now all three implemented.