Minesweeper: verify its logic on the host, and document it in both languages

apps/minesweeper/host_test.c includes the app source with a fake app_api_t, so the real state machine runs on a PC: every string it draws is recorded and the lit pixels are counted. Measured -- a reveal/flag/new-game/digit/quit script returns normally, draws the title, the mine count and lights 24 pixels; a script that blindly reveals 85 cells reaches a terminal state eleven times, draws BOOM, and MENU starts a new game after it (terminal at record 356, title again at 4180). The win path is the one branch blind play does not reach.

Both READMEs now say what is verified (compiles clean under gcc -Wall -Wextra -Werror against upstream's real app_api.h, which is what caught the API's true member names and the absence of left/right keys; the logic runs on the host) and what is not (never built for ARM, never run on the radio -- no toolchain and no Docker here).
This commit is contained in:
mckero committed 2026-10-01 22:31:22 +08:00
1 parent ff14dffb67
commit 61344e486e
3 files changed
+161

No files matched your search

+15
View File
@@ -44,3 +44,18 @@ that `APP_KEY_LEFT`/`APP_KEY_RIGHT` do not exist).
Not verified: it has never been built for ARM or run on the radio, because no Not verified: it has never been built for ARM or run on the radio, because no
`arm-none-eabi-gcc` and no Docker exist on the machine it was written on. Treat the `arm-none-eabi-gcc` and no Docker exist on the machine it was written on. Treat the
first build and the first run as the real review. first build and the first run as the real review.
## The host harness (how far verification got)
`host_test.c` includes the app source and hands it a fake `app_api_t`, so the real state
machine runs on the PC -- every string it draws is recorded and the lit pixels are counted:
gcc -std=gnu11 -O1 -Wall -Wextra -Werror -I.. -o host_test host_test.c && ./host_test
Measured: a reveal/flag/new-game/digit/quit script returns normally, draws the title and the
mine count, and lights pixels; a script that blindly reveals 85 cells reaches a terminal state
eleven times, draws `BOOM`, and MENU starts a new game afterwards. The win path (`CLEAR`) was
not reached by blind play, so it is the one branch this harness does not exercise.
Still unverified: never built for ARM, never run on the radio -- no `arm-none-eabi-gcc` and no
Docker where it was written. The first build and the first run are the real review.
+50
View File
@@ -0,0 +1,50 @@
# 扫雷 —— F4HWN Labs 版的叠加应用
我们自己的应用 ✓:9×9 扫雷 ✓,跑在 `App/apps/app_overlay.h` 预留的 **4 KiB 叠加区**里 ✓。
它是按上游的 `App/apps/app_api.h` 写的 ✓、用上游的 `app.ld` 链接 ✓ —— **这两个上游文件没有随本仓库分发** ✗
(它们来自 [armel/uv-k1-k5v3-firmware-custom](https://github.com/armel/uv-k1-k5v3-firmware-custom),Apache-2.0 ✓),
所以把这个目录放进 `App/apps/minesweeper/` 与它们并列 ✓,或把 `-I` 指向一份副本 ✓。
## 为什么它长这样
| 约束 | 后果 |
| --- | --- |
| 这台电台**没有左右键** ✓(只有 UP、DOWN、MENU、EXIT、STAR、F、0-9 ✓) | 光标用 UP/DOWN 走 ✓,数字**先选行再选列** ✓:`3` `5` = 第 3 行第 5 列 ✓ |
| **4 KiB**(text+rodata+data+bss 合计 ✓) | 不用查表 ✓、不用浮点 ✓、不链 libc ✓;邻雷数现算 ✓,每格一个 bit ✓ |
| 81 格放不进 16 位掩码 ✓ | 三个 9 字节位数组 ✓,按 `cell >> 3`、`cell & 7` 寻址 ✓ —— 早先的 `uint16_t` 版本**能编过但在第 15 格之后是错的** ✗ |
| 常驻的像素函数**不做边界检查** ✓ | `put()`/`invert()` 自己裁剪 ✓ |
| freestanding 里没有 `rand()` ✓ | 一个小 LCG ✓;雷在**第一次翻开之后**才布 ✓,并保证首翻周围 3×3 无雷 ✓ |
按键:UP/DOWN 移动 ✓、1-9 先选行再选列 ✓、MENU 翻开 ✓、F 插旗 ✓、STAR 重开 ✓、EXIT 退出 ✓。
角上的 `M` 是剩余雷数 ✓,`A1` 是光标位置 ✓。
## 构建
arm-none-eabi-gcc -mcpu=cortex-m0plus -mthumb -Os -std=gnu11 -ffreestanding \
-nostdlib -nostartfiles -T app.ld -Wl,--defsym,APP_VMA=0x20000280 \
-o minesweeper.elf minesweeper_app.c
arm-none-eabi-objcopy -O binary minesweeper.elf minesweeper.bin
pack_app.py minesweeper.bin Minesweeper.app --name Minesweeper --ver 1.0 \
--vma 0x20000280 --api-min 1 # pack_app.py 在 App/apps/ 下
`build.sh` 做的就是这些 ✓,需要 PATH 上有 Arm GNU Toolchain ✓。
然后**从网页安装** ✓:*Overlay apps* → 选一个槽 → 选 `Minesweeper.app` → **Install** →
**Ask the radio** 应当回 `Minesweeper` ✓。在电台上按 **F** 再按 **7**、再按 **MENU** 运行 ✓。
## 验证到什么程度(`host_test.c` 可复现)
`host_test.c` 把应用源码直接包进来 ✓、给它一个假的 `app_api_t` ✓,在 PC 上**真的跑它的状态机** ✓
(记录它每一次画出的字符串、统计点亮的像素 ✓):
gcc -std=gnu11 -O1 -Wall -Wextra -Werror -I.. -o host_test host_test.c && ./host_test
实测输出 ✓:脚本一(翻开/插旗/重开/数字选格/退出)正常返回 ✓、标题与雷数都画了 ✓、有像素点亮 ✓;
脚本二(盲翻 85 格)到达终局 11 次 ✓、`BOOM` 已绘制 ✓、终局后按 MENU 回到新局 ✓。
**已经验证** ✓:源码在 `gcc -Wall -Wextra -Werror` 下干净通过 ✓(这一步抓出了 API 的真实成员名 ✓
`api->fb` ✓、`print_tiny(s, x, y, statusbar, fill)` **五个**参数 ✓,以及 `APP_KEY_LEFT`/`APP_KEY_RIGHT`
**根本不存在** ✓);游戏逻辑在 PC 上跑通 ✓。
**没有验证** ✗:从未为 ARM 编译过 ✓、也没在电台上跑过 ✓ —— 写它的机器上既没有 `arm-none-eabi-gcc`
也没有 Docker ✓。**第一次构建与第一次上机就是真正的评审** ✓。
+96
View File
@@ -0,0 +1,96 @@
/* Host harness: run the minesweeper logic on the PC, without ARM or the radio.
* Not shipped -- it lives in work/ (git-ignored). It includes the app source directly
* and supplies a fake app_api_t, so the game's real state machine executes: keys go in,
* the strings it draws come out, and the framebuffer can be counted.
*/
#include <stdio.h>
#include <string.h>
#include <stdint.h>
#include <stdbool.h>
/* the app's own includes pull ../app_api.h, which resolves from this directory */
#include "minesweeper_app.c"
static uint8_t fb[64][128];
static char drawn[8192][24]; /* the game redraws every frame; 64 was my limit, not its */
static int drawn_n;
static const uint8_t *keys;
static int keys_n, keys_i;
static int tones;
static void t_clear(void) { memset(fb, 0, sizeof fb); }
static void t_tiny(const char *s, uint8_t x, uint8_t y, bool statusbar, bool fill)
{
(void)x; (void)y; (void)statusbar; (void)fill;
if (drawn_n < 8192) snprintf(drawn[drawn_n++], 24, "%s", s);
}
static uint8_t t_key(void) { return keys_i < keys_n ? keys[keys_i++] : APP_KEY_EXIT; }
static void t_delay(uint32_t ms) { (void)ms; }
static void t_blit(void) {}
static void t_tone(uint16_t hz, uint16_t ms) { (void)hz; (void)ms; tones++; }
static bool saw(const char *needle)
{
for (int i = 0; i < drawn_n; i++)
if (strcmp(drawn[i], needle) == 0)
return true;
return false;
}
int main(void)
{
app_api_t api;
memset(&api, 0, sizeof api);
api.fb = fb;
api.display_clear = t_clear;
api.print_tiny = t_tiny;
api.blit_full = t_blit;
api.get_key = t_key;
api.delay_ms = t_delay;
api.play_tone = t_tone;
/* 1) a reveal, a flag, a new game, then quit -- the state machine must return */
static const uint8_t script1[] = { APP_KEY_MENU, APP_KEY_DOWN, APP_KEY_DOWN, APP_KEY_F,
APP_KEY_STAR, APP_KEY_3, APP_KEY_5, APP_KEY_MENU,
APP_KEY_EXIT };
keys = script1; keys_n = sizeof script1; keys_i = 0; drawn_n = 0; tones = 0;
t_clear();
app_main(&api);
int lit = 0;
for (int y = 0; y < 64; y++)
for (int x = 0; x < 128; x++)
if (fb[y][x >> 3] & (1u << (7 - (x & 7)))) lit++;
printf("script 1 (reveal/flag/new/digits/quit): returned normally, tones=%d\n", tones);
printf(" title drawn : %s\n", saw("F4HWN MINES") ? "yes" : "no");
printf(" mine count : %s (the app draws \"M\" and the number separately)\n", saw("10") ? "yes" : "no");
printf(" lit pixels : %d (rendering happened: %s)\n", lit, lit > 0 ? "yes" : "NO");
/* 2) reveal a lot of cells: the game must reach a terminal state, and a mine hit
* must show BOOM; then MENU must start a new game and the title must come back */
uint8_t script2[2 + 2 * 85 + 2 + 16]; /* sized for what the loops below actually write */
int n = 0;
script2[n++] = APP_KEY_MENU; /* first reveal is safe by design */
for (int i = 0; i < 85; i++) { /* walk and reveal everything */
script2[n++] = APP_KEY_DOWN;
script2[n++] = APP_KEY_MENU;
}
script2[n++] = APP_KEY_MENU; /* after the end: new game */
for (int i = 0; i < 12; i++) script2[n++] = APP_KEY_INVALID;
keys = script2; keys_n = n; keys_i = 0; drawn_n = 0; tones = 0;
t_clear();
app_main(&api);
printf("\nscript 2 (reveal 85 cells): tones=%d (%s)\n", tones,
tones > 0 ? "a terminal state played a tone" : "no terminal state reached");
printf(" BOOM drawn : %s\n", saw("BOOM") ? "yes" : "no");
printf(" CLEAR drawn : %s\n", saw("CLEAR") ? "yes" : "no");
/* after a terminal state the title must come back, i.e. MENU started a new game */
int first_title = -1, later_title = -1, terminal_at = -1;
for (int i = 0; i < drawn_n; i++) {
if (!strcmp(drawn[i], "F4HWN MINES")) { if (first_title < 0) first_title = i; else later_title = i; }
if (!strcmp(drawn[i], "BOOM") && terminal_at < 0) terminal_at = i;
}
printf(" new game after a terminal state: %s (terminal at %d, title again at %d)\n",
(terminal_at >= 0 && later_title > terminal_at) ? "yes" : "NO", terminal_at, later_title);
printf(" frames drawn: %d strings recorded\n", drawn_n);
return 0;
}