The counts beside the census, and the language claim the walk used to carry

This commit is contained in:
Joseph Ferano 2026-09-14 08:40:32 +07:00
parent c355739f55
commit 7ebf7ec9c4
3 changed files with 15 additions and 7 deletions

View File

@ -827,10 +827,17 @@ call fit it exactly.
is `(and (> i 0) (continuation? (at b i)))`, and at the start of the text `i` is -1 — so if is `(and (> i 0) (continuation? (at b i)))`, and at the start of the text `i` is -1 — so if
`and` were a strict function rather than a form, the guard would not save the `(at b -1)` `and` were a strict function rather than a form, the guard would not save the `(at b -1)`
beside it and the first press of LEFT would signal `BoundsError`. It is a form and it does beside it and the first press of LEFT would signal `BoundsError`. It is a form and it does
short-circuit; `test/programs/raylib-codepoints.flan` has a row for it, because the walk short-circuit; `test/programs/raylib-codepoints.flan` had a row for it, because the walk
itself never reaches that offset and the claim is about the language rather than about the itself never reaches that offset and the claim is about the language rather than about the
example. example.
> **Note, 2026-09-14.** The walk this describes is gone — §A.1 above closed, and `step-back`
> is now one call to `GetCodepointPrevious`. The finding stands and the observation about
> `and` is still true; what went with the walk is the corpus's only exercise of it over an
> out-of-bounds index. The `back at start 0` row still runs and now pins the `(<= offset 0)`
> guard instead, which is the right thing for it to pin. A language claim wants a language
> test rather than a raylib example, and there is not one.
**Fixed arrays were the right shape for both.** A codepoint table with a count, a **Fixed arrays were the right shape for both.** A codepoint table with a count, a
`[9 Rectangle]` of toggle buttons, a `[9 string]` of labels. The §3 finding from the `[9 Rectangle]` of toggle buttons, a `[9 string]` of labels. The §3 finding from the
siam-farmer report — a global cannot hold a `Vec`, and fixed arrays with counts are usually siam-farmer report — a global cannot hold a `Vec`, and fixed arrays with counts are usually

View File

@ -111,11 +111,12 @@ actually about is a **pointer reinterpretation**, which is not a checker arm.
- `dune build --root .` and `dune test --root .` clean; the dev suite is 232 checks, 0 - `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 failures, unchanged — the new checks are in `test_flan.ml`, which reports pass/fail
rather than a count. rather than a count.
- Eleven new checks in `test/test_flan.ml` over three new functions in - New checks in `test/test_flan.ml` over three new functions in `test/headers/sample.h`
`test/headers/sample.h` (`blit`, `scratch`, `pair_len_p`): six that must agree, five (`blit`, `scratch`, `pair_len_p`): six declarations that must agree, five that must
that must still be reported, each asserting on the message and not on a count. All still be reported, each asserting on the message and not on a count. All of them were
eleven were confirmed live by breaking `ptr_agrees` in three different directions and confirmed live by breaking `ptr_agrees` in three different directions and watching the
watching the right subset go red. right subset go red — the negatives matter most, and they are why the arm can be widened
without the check becoming decoration.
- The raylib acceptance cases ran rather than skipped (`ldconfig` finds - 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 `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. wants a wasm build of raylib that is not in this tree.

View File

@ -24,7 +24,7 @@
# out of this header and agrees with it by construction. That is also why # out of this header and agrees with it by construction. That is also why
# the hand-written lines 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 # (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 # moved on to 464 and 197, which is what a census written into a comment
# beside a growing file always does.) # beside a growing file always does.)
# #
# Why it is no longer optional. It used to be `?${FLAN_RAYLIB_H}`, and the # Why it is no longer optional. It used to be `?${FLAN_RAYLIB_H}`, and the