The two gaps read as closed, and a census that had rotted stops being a census

docs/PORTING.md

@@ -660,6 +660,18 @@ each finding in §A names the command that produced the failure.
 
 ### A.1 `GetCodepointPrevious` cannot be called, and closing it is a checker change
 
+> **Closed, 2026-09-14.** It was a checker change and it is made: `agrees` in
+> `lib/cimport.ml` now has the pointer arm its own comment had been listing among the
+> differences it accepted. `vendor/raylib/raylib.flan` carries
+> `get-codepoint-previous-raw` — the exact declaration this section says it wanted — and
+> a `get-codepoint-previous` wrapper over it that takes the bytes and an offset;
+> `generated.flan` no longer carries the `string`-faced version at all, because a binding
+> that is wrong for the only direction it reads in is worse than no binding. The example's
+> `step-back` is one call to it, the continuation-byte walk is gone, and the expression
+> below now prints 12356 and 3. The section is kept as written; the reasoning is the part
+> worth having.
+
+
 This is the real find of the round, and it is general: **a C function that reads
 *backwards* from the pointer it is handed cannot be given a Flan `string`.**
 
@@ -739,6 +751,26 @@ binding over a `const char *` cursor meets it.
 
 ### A.2 There is no cast between pointer types
 
+> **Half closed, 2026-09-14, and the other half turned out to be somewhere else.** The
+> header check does now accept it: a C `void *` is opaque about *what* it points at, so
+> `ptr_agrees` lets a `(Ptr` anything `)` stand against one, and that was the refusal this
+> section hit. What the refusal was masking is that `lib/shim.ml` will not take a second
+> `declare-c` for a C symbol it already has — 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. So the natural binding fix named below is refused
+> after all, by a rule that is right.
+>
+> Its own message says what to write instead — "another Flan name for it is a defn" — and
+> `vendor/raylib/raylib.flan` now has `update-texture-colors`, a one-line defn over the
+> generated `update-texture` that spells the conversion as `(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 that
+> cannot be written. The example's call site is `(rl/update-texture-colors texture pixels)`
+> and the slice-and-index is gone; the cast still exists, once, with a name and a comment
+> on it. **What is still open is the general thing this section is about** — a pointer
+> reinterpretation — and it is not a checker arm.
+
+
 `textures_image_processing` hands the pixels `LoadImageColors` returned straight to
 `UpdateTexture`. In C both are pointers and nothing has to be said. Here
 `load-image-colors` answers `(Ptr Color)` and `update-texture` takes `(Ptr u8)` — the
@@ -866,8 +898,10 @@ load a file out of `resources/` and neither file is in this tree.
   boxes and the program explains itself rather than looking broken.
 
 **Neither example needed a language feature.** Nothing below the two refused bindings in §A
-was blocked at all, and both of those are one arm in `lib/cimport.ml`'s `agrees` away from
+was blocked at all, and both of those were one arm in `lib/cimport.ml`'s `agrees` away from
-being ordinary binding work.
+being ordinary binding work. That arm was written on 2026-09-14 and §A.1 is now ordinary
+binding work; §A.2 turned out to have a second, better reason behind the first, and the
+boxes at the head of each section say what happened.
 
 ## E. Testing
 

vendor/raylib/headers

@@ -17,12 +17,15 @@
 #   2. every ordinary build. Every C symbol
 #      is bound already — by hand in raylib.flan or by generation in
 #      generated.flan — so the importer generates nothing and the header read
-#      is purely the check. It runs over all 425 declarations rather than the
+#      is purely the check. It runs over every declaration in the package and
-#      172 hand-written ones, because the generated file is a package file like
+#      not only the hand-written ones, because the generated file is a package
-#      any other and is checked like one — though only the hand-written ones can
+#      file like any other and is checked like one — though only the
-#      actually disagree, since the generated half came out of this header and
+#      hand-written ones can actually disagree, since the generated half came
-#      agrees with it by construction. That is also why the hand-written lines
+#      out of this header and agrees with it by construction. That is also why
-#      were kept rather than replaced by generated ones.
+#      the hand-written lines were kept rather than replaced by generated ones.
+#      (There were counts here once. They said 425 and 172 and the truth had
+#      moved on to 463 and 196, which is what a census written into a comment
+#      beside a growing file always does.)
 #
 # Why it is no longer optional. It used to be `?${FLAN_RAYLIB_H}`, and the
 # argument was that a build needs libraylib linkable and *not* raylib-devel