docs+analysis: independent verification guide for phases A-F (calibrated scanners, self-tested commands)

This commit is contained in:
ZXCLI
2026-09-11 01:10:18 +08:00
parent 8e1312a137
commit 0919f5e186
4 changed files with 789 additions and 11 deletions
@@ -6,8 +6,28 @@
**`libcxsdk.so` 里没有静态调色板表**。12 个调色板全部由
`CFunctions::SetColorPalette`Ghidra 偏移 `0x00026c70`)在**运行时用算术生成**。
对全文件扫描"连续 256 个 u32LE、alpha=0xFF 且 RGB 非零"的候选 **命中 0 个**
alpha=0x00 形式、BGR/RGB 三元组形式同样为 0)。
两层证据(2026-09-11 复核时补强,见"否证的最强形式"):
1. **正对照(决定性)**:项目持有的唯一官方表——铁虹——
csdk `src/mag160c_official_palette256.h`,源自厂商运行时内存
`CoreSDKLib dev+0xb18`)在库里**以任何编码都搜不到**
- `B,G,R,0`(官方文档布局)→ 无
- `B,G,R,0xFF`alpha 强制)→ 无
- **忽略第 4 字节的 `B,G,R` 宽松匹配 → 也无**
⚠️ **踩坑记录**:该表在内存里是 `(B, G, R, 0)` —— **第 4 字节是 0**
`OfficialTables.kt` 里的 ARGB int 被生成脚本强制 `alpha=0xFF`
因此"直接拿 Kotlin 表去二进制里搜"**永远搜不到**,会得出假的"未找到"。
正确的针必须从 csdk 头文件(真实内存布局)构造。核查时务必用
`analysis/tools/PalScan.java`(已按此修正)而非手工拼的 ARGB 针。
2. **结构性证据**:Ghidra 反编译显示该函数用算术逐条生成全部 12 张表
`libcxsdk_decomp.txt` 的 case 0..10/12/13),所以静态数据里本就不该有。
> 另:早期"扫描 256 个连续 u32LE、alpha=0xFF"的判据命中 0,这一条仍成立但
> **说服力弱**——它只说明"没有 alpha=0xFF 形式",与布局无关。
> 通用"渐变"启发式(`PalScan.java` 的 [C] 段)在本库上误报约 11% 的位置
> (全是指令/整数数组),**不能作为证据**,工具里已明确如此标注。
因此本阶段改用**移植生成函数**的路线并成功恢复:
**UI 索引 0..10 共 11 个调色板已为官方精确表**(索引 11 见下),
@@ -62,22 +82,38 @@
| `analysis/sdk_re/android_app/palette_candidates.json` | 扫描结论(静态候选为空)+ 全部恢复表 |
| `analysis/sdk_re/android_app/palette_candidates.png` | 12 组「官方预览图 + 恢复色条」对照图 |
| `analysis/sdk_re/android_app/palette_match_report.txt` | 覆盖率证据表 |
| `analysis/tools/extract_palettes.py` | 计划要求的纯标准库扫描脚本(可复现"无静态表"这一否定结论 |
| `analysis/tools/extract_palettes.py` | 计划要求的纯标准库扫描脚本(本机无 python3,改用下面的 JDK 版 |
| `analysis/tools/PalScan.java` | **JDK 版否证复核器**:正对照(铁虹在 3 种编码下的精确匹配)+ 自校准 + 通用扫描(明确标注不可作证据)。已实测:3 种编码全部 not found |
| `analysis/tools/PalIdentify.java` | 13 个生成体的机械移植(含写地址校验) |
| `analysis/tools/PalExport2.java` | 导出 Kotlin/JSON/PNG/报告 |
| `analysis/tools/PalExport2.java` | 导出 Kotlin/JSON/PNG/报告(须与 PalIdentify 一起编译) |
| `analysis/tools/CheckStrings.java` | 核对真机清单里的日志串是否真能由源码产生 |
| `android/.../core/VendorPalettes.kt` | 生成的 Kotlin 表(0..10 为精确表) |
重跑(本机无 python3Java 版单文件即可运行):
重跑(本机无 python3;两个命令都已实测通过):
```bash
java analysis/tools/PalExport2.java \
android/app/src/main/kotlin/com/mag160c/thermal/core/OfficialTables.kt \
<解包APK的 res/mipmap-hdpi-v4 目录> \
android/app/src/main/kotlin/com/mag160c/thermal/core \
analysis/sdk_re/android_app
# 否证复核:铁虹是否真的不在库里(决定性证据)
java analysis/tools/PalScan.java \
analysis/sdk_re/android_app/bin/libcxsdk.so \
csdk/src/mag160c_official_palette256.h
# 生成物可复现:重新生成后与仓库文件 diff 应为空
mkdir -p /c/Users/zxc/AppData/Local/Temp/regen_build && \
cd /c/Users/zxc/AppData/Local/Temp/regen_build && \
cp "C:\Project\MAG160C\analysis\tools\PalIdentify.java" . && \
cp "C:\Project\MAG160C\analysis\tools\PalExport2.java" . && \
"C:\Tools\jdk-21\bin\javac" -d out PalIdentify.java PalExport2.java && \
"C:\Tools\jdk-21\bin\java" -cp out PalExport2 \
"C:\Project\MAG160C\android\app\src\main\kotlin\com\mag160c\thermal\core\OfficialTables.kt" \
"C:\Users\zxc\AppData\Local\Temp\cxres\res\mipmap-hdpi-v4" \
"C:\Users\zxc\AppData\Local\Temp\regen_core" \
"C:\Users\zxc\AppData\Local\Temp\regen_out"
diff "C:\Users\zxc\AppData\Local\Temp\regen_core\VendorPalettes.kt" \
"C:\Project\MAG160C\android\app\src\main\kotlin\com\mag160c\thermal\core\VendorPalettes.kt"
# 实测:diff 为空;铁虹锚点 256/256
```
有 python3 的机器上:
有 python3 的机器上(可选,仅证明"无静态 256 项 alpha=0xFF 表"这个弱结论)
```bash
python3 analysis/tools/extract_palettes.py \
+75
View File
@@ -0,0 +1,75 @@
import java.nio.file.*;
import java.util.*;
import java.util.regex.*;
import java.util.stream.*;
/**
* Cross-check the quoted DebugLog lines in docs/android_app/real_device_checklist.md
* against the Kotlin sources, so a verifier can confirm the checklist describes
* logs the code can actually produce.
*
* WHY NOT A PLAIN SEARCH: the sources build messages by interpolation
* ("$name write=$n/${packet.size}") while the checklist shows instantiated
* examples ("GetParameter1 write=4/4"). A literal search therefore produces
* false negatives. This tool instead (1) tries the literal with <placeholders>
* removed, then (2) falls back to requiring the remaining identifier-ish words
* to appear somewhere in the sources.
*
* A "needs review" line means the whole message is instance data (the template
* lives in one string literal and the command name is a call-site argument) —
* those must be traced by hand to the call site. Both categories were manually
* resolved for the 2026-09-11 run (see verification_guide.md §3 Phase A).
*
* Usage:
* java CheckStrings.java docs/android_app/real_device_checklist.md android/app/src/main
*/
public class CheckStrings {
public static void main(String[] a) throws Exception {
String md = Files.readString(Paths.get(a[0]), java.nio.charset.StandardCharsets.UTF_8);
StringBuilder src = new StringBuilder();
try (Stream<Path> s = Files.walk(Paths.get(a[1]))) {
List<Path> kt = s.filter(x -> x.toString().endsWith(".kt")).collect(Collectors.toList());
for (Path p : kt) src.append(Files.readString(p, java.nio.charset.StandardCharsets.UTF_8)).append('\n');
}
String all = src.toString();
// only lines that show a DebugLog tag: [usb] [vm] [session] [cmd] [stream] [pip] [remote] [crash]
Matcher m = Pattern.compile("`(\\[(?:usb|vm|session|cmd|stream|pip|remote|crash)\\][^`]*)`").matcher(md);
int exact = 0, skeleton = 0, miss = 0;
Set<String> seen = new LinkedHashSet<>();
List<String> misses = new ArrayList<>();
while (m.find()) {
String line = m.group(1);
if (!seen.add(line)) continue;
// the tag is a separate DebugLog argument in the source
String msg = line.replaceFirst("^\\[[a-z]+\\]\\s*", "");
String literal = msg.replaceAll("<[^>]*>", "").trim();
if (literal.length() >= 6 && all.contains(literal)) { exact++; continue; }
String skel = msg
.replaceAll("<[^>]*>", " ")
.replaceAll("0x[0-9A-Fa-f]+", " ")
.replaceAll("\\b\\d+(\\.\\d+)?\\b", " ")
.replaceAll("[A-Za-z]*\\d[A-Za-z0-9]*", " ")
.replaceAll("[^\\x20-\\x7E\\u4e00-\\u9fff]+", " ");
List<String> keep = new ArrayList<>();
for (String w : skel.trim().split("\\s+")) {
if (w.length() >= 3 && w.matches("[A-Za-z_:.\\-\\[\\]()/]+")) keep.add(w);
}
boolean found = !keep.isEmpty();
for (String w : keep) if (!all.contains(w)) found = false;
if (found) skeleton++;
else { miss++; misses.add(line + " [probe: " + String.join(" ", keep) + "]"); }
}
System.out.println("exact literal match : " + exact);
System.out.println("skeleton match : " + skeleton);
System.out.println("needs human review : " + miss);
if (!misses.isEmpty()) {
System.out.println();
for (String s : misses) System.out.println(" ? " + s);
}
}
}
+244
View File
@@ -0,0 +1,244 @@
import java.nio.file.*;
import java.util.*;
/**
* Independent check of the Phase C negative claim: "libcxsdk.so contains no
* static palette tables."
*
* The canonical scanner is analysis/tools/extract_palettes.py, but this machine
* has no working python3, so this JDK equivalent lets a verifier re-run the scan.
*
* The tool reports three things and is explicit about how much each one proves.
*
* [A] DETECTOR SANITY -- the known iron-bow table is planted into a synthetic
* buffer and the broad scan must find it. This only proves the scan is not
* blind; it proves nothing about the library.
*
* [B] POSITIVE CONTROL (the decisive part) -- the same table is searched for
* verbatim in the library under the DOCUMENTED byte layout. This matters:
* csdk/src/mag160c_official_palette256.h records the vendor table as
* "256 x 4 bytes (B, G, R, 0)" — the 4th byte is ZERO, while the ARGB ints
* in OfficialTables.kt have alpha forced to 0xFF by the generator, so
* searching the Kotlin ints directly can never match the binary. The tool
* therefore rebuilds the needle from the csdk header (ground truth) and
* additionally tries an RGB-only match that ignores the 4th byte.
* Iron-bow is the one vendor palette the project holds (captured at runtime
* from CoreSDKLib dev+0xb18, verified pixel-exact against the official
* renderer); if this library stored static tables of that family, it would
* be among them. Absence in every encoding is therefore strong evidence
* for the negative claim.
*
* [C] BROAD SCAN (reported, but NOT usable as evidence) -- a generic "256-entry
* colour ramp" search. Measured on this library it flags ~11% of all
* positions, all of them ARM32 code where the 4th byte of each word happens
* to be constant and adjacent words differ little. A generic ramp test
* cannot separate palettes from integer/address arrays, so this count is
* deliberately reported with its false-positive density instead of being
* presented as a verdict.
*
* The negative claim therefore rests on [B] plus the independent structural
* evidence: the Ghidra listing shows CFunctions::SetColorPalette COMPUTING all
* twelve tables with arithmetic (analysis/sdk_re/android_app/libcxsdk_decomp.txt),
* which is why no static data can be found.
*
* Usage:
* java PalScan.java analysis/sdk_re/android_app/bin/libcxsdk.so \
* csdk/src/mag160c_official_palette256.h
*/
public class PalScan {
static final int N = 256;
static final int STEP_LIMIT = 0x200000; // max per-step change
static final int CHANNEL_SPAN = 64; // a colour scale spans a channel
static final int MIN_SPANNING_CHANNELS = 2;
public static void main(String[] args) throws Exception {
String libPath = args[0];
String headerPath = args.length > 1 ? args[1] : null;
byte[] lib = Files.readAllBytes(Paths.get(libPath));
System.out.println("file: " + libPath + " (" + lib.length + " bytes)");
if (headerPath == null) {
System.out.println("(pass csdk/src/mag160c_official_palette256.h as the 2nd argument)");
return;
}
// Ground truth for the in-binary layout: the csdk header holds the table
// exactly as it appears in memory, (B, G, R, 0) per entry.
int[][] rgb = readHeader(headerPath);
if (rgb.length != N) {
System.out.println("header parsed " + rgb.length + " entries, expected " + N + " - aborting");
return;
}
System.out.println("ground-truth table: " + N + " entries (B,G,R,0), first 3 = "
+ rgb[0][0] + "," + rgb[0][1] + "," + rgb[0][2] + " "
+ rgb[1][0] + "," + rgb[1][1] + "," + rgb[1][2] + " "
+ rgb[2][0] + "," + rgb[2][1] + "," + rgb[2][2]);
// ---------- [A] detector sanity ----------
byte[] planted = encodeHeader(rgb, false);
int plantedHits = scan(planted).size();
System.out.println();
System.out.println("[A] detector sanity: planted the known table into a 1024-byte buffer");
System.out.println(" detected: " + plantedHits + " candidate(s)"
+ (plantedHits == 0 ? " <-- SCAN IS BLIND, [C] is meaningless" : " (scan is not blind)"));
// ---------- [B] positive control ----------
System.out.println();
System.out.println("[B] POSITIVE CONTROL - is the known vendor table stored verbatim?");
int exact = indexOf(lib, encodeHeader(rgb, false), 0);
System.out.println(" B,G,R,0 (documented layout) : "
+ (exact < 0 ? "not found" : "*** FOUND at 0x" + Integer.toHexString(exact) + " ***"));
int exactFF = indexOf(lib, encodeHeader(rgb, true), 0);
System.out.println(" B,G,R,0xFF (alpha forced) : "
+ (exactFF < 0 ? "not found" : "*** FOUND at 0x" + Integer.toHexString(exactFF) + " ***"));
int rgbOnly = matchRgbIgnoringFourth(lib, rgb);
System.out.println(" B,G,R ignoring 4th byte : "
+ (rgbOnly < 0 ? "not found" : "*** FOUND at 0x" + Integer.toHexString(rgbOnly) + " ***"));
// ---------- [C] broad scan ----------
System.out.println();
System.out.println("[C] broad scan for any 256-entry colour ramp (supporting only):");
List<Integer> hits = scan(lib);
int positions = (lib.length - N * 4) / 4;
System.out.printf(" candidates: %d of %d positions (%.1f%%)%n",
hits.size(), positions, 100.0 * hits.size() / Math.max(1, positions));
if (!hits.isEmpty()) {
System.out.println(" These are ARM32 code regions: the ramp test cannot tell a colour");
System.out.println(" scale from a run of small integers, so this count is NOT evidence.");
}
// ---------- verdict ----------
System.out.println();
boolean found = exact >= 0 || exactFF >= 0 || rgbOnly >= 0;
if (found) {
System.out.println("VERDICT: a static copy of the vendor table IS present -> the negative claim is WRONG.");
} else {
System.out.println("VERDICT: the known vendor table is absent in every encoding tested.");
System.out.println(" Together with the Ghidra listing (CFunctions::SetColorPalette computes");
System.out.println(" the tables arithmetically) this upholds the negative claim:");
System.out.println(" libcxsdk.so stores no static palette tables.");
}
}
/** Parse csdk/src/mag160c_official_palette256.h into {B,G,R} triples. */
static int[][] readHeader(String path) throws Exception {
List<int[]> rows = new ArrayList<>();
for (String line : Files.readAllLines(Paths.get(path), java.nio.charset.StandardCharsets.UTF_8)) {
if (!line.contains("{") || !line.contains("}")) continue;
String body = line.substring(line.indexOf('{') + 1, line.indexOf('}'));
String[] parts = body.split(",");
if (parts.length < 3) continue;
try {
rows.add(new int[]{
Integer.parseInt(parts[0].trim()),
Integer.parseInt(parts[1].trim()),
Integer.parseInt(parts[2].trim()),
});
} catch (NumberFormatException e) {
// header/trailer lines
}
}
return rows.toArray(new int[0][]);
}
static byte[] encodeHeader(int[][] rgb, boolean alphaFF) {
byte[] out = new byte[rgb.length * 4];
for (int i = 0; i < rgb.length; i++) {
out[i*4] = (byte) rgb[i][0];
out[i*4+1] = (byte) rgb[i][1];
out[i*4+2] = (byte) rgb[i][2];
out[i*4+3] = (byte) (alphaFF ? 0xFF : 0x00);
}
return out;
}
/** Match all 256 (B,G,R) triples at 4-byte stride, ignoring the 4th byte. */
static int matchRgbIgnoringFourth(byte[] data, int[][] rgb) {
for (int o = 0; o + rgb.length * 4 <= data.length; o += 4) {
boolean ok = true;
for (int i = 0; i < rgb.length && ok; i++) {
int p = o + i * 4;
if ((data[p] & 0xFF) != rgb[i][0]
|| (data[p+1] & 0xFF) != rgb[i][1]
|| (data[p+2] & 0xFF) != rgb[i][2]) ok = false;
}
if (ok) return o;
}
return -1;
}
/** All offsets whose 1024-byte window passes the ramp test. */
static List<Integer> scan(byte[] b) {
List<Integer> out = new ArrayList<>();
for (int o = 0; o + N * 4 <= b.length; o += 4) if (isPaletteRun(b, o)) out.add(o);
return out;
}
static boolean isPaletteRun(byte[] b, int o) {
int alpha = b[o + 3] & 0xFF;
int prev = -1, distinct = 0;
int[] mn = {255, 255, 255}, mx = {0, 0, 0};
for (int i = 0; i < N; i++) {
int p = o + i * 4;
if ((b[p + 3] & 0xFF) != alpha) return false; // unused byte constant
int bl = b[p] & 0xFF, g = b[p + 1] & 0xFF, r = b[p + 2] & 0xFF;
int v = bl | (g << 8) | (r << 16);
if (prev >= 0 && Math.abs(v - prev) > STEP_LIMIT) return false;
if (v != prev) distinct++;
if (bl < mn[0]) mn[0] = bl; if (bl > mx[0]) mx[0] = bl;
if (g < mn[1]) mn[1] = g; if (g > mx[1]) mx[1] = g;
if (r < mn[2]) mn[2] = r; if (r > mx[2]) mx[2] = r;
prev = v;
}
if (distinct < 32) return false;
int spanning = 0;
for (int c = 0; c < 3; c++) if (mx[c] - mn[c] >= CHANNEL_SPAN) spanning++;
return spanning >= MIN_SPANNING_CHANNELS;
}
static byte[] encode(int[] anchor, int order) {
byte[] out = new byte[anchor.length * 4];
for (int i = 0; i < anchor.length; i++) {
int v = anchor[i];
int r = (v >> 16) & 0xFF, g = (v >> 8) & 0xFF, bl = v & 0xFF, al = (v >>> 24) & 0xFF;
switch (order) {
case 0: putLE(out, i * 4, v); break;
case 1: putBE(out, i * 4, v); break;
case 2: out[i*4]=(byte) bl; out[i*4+1]=(byte) g; out[i*4+2]=(byte) r; out[i*4+3]=(byte) al; break;
case 3: out[i*4]=(byte) r; out[i*4+1]=(byte) g; out[i*4+2]=(byte) bl; out[i*4+3]=(byte) al; break;
case 4: out[i*4]=0; out[i*4+1]=(byte) bl; out[i*4+2]=(byte) g; out[i*4+3]=(byte) r; break;
}
}
return out;
}
static void putLE(byte[] o, int p, int v) {
o[p]=(byte)(v&0xFF); o[p+1]=(byte)((v>>8)&0xFF); o[p+2]=(byte)((v>>16)&0xFF); o[p+3]=(byte)((v>>>24)&0xFF);
}
static void putBE(byte[] o, int p, int v) {
o[p]=(byte)((v>>>24)&0xFF); o[p+1]=(byte)((v>>16)&0xFF); o[p+2]=(byte)((v>>8)&0xFF); o[p+3]=(byte)(v&0xFF);
}
static int indexOf(byte[] hay, byte[] needle, int from) {
outer:
for (int i = from; i + needle.length <= hay.length; i++) {
for (int j = 0; j < needle.length; j++) if (hay[i + j] != needle[j]) continue outer;
return i;
}
return -1;
}
static int[] readAnchor(String ktPath) throws Exception {
String src = Files.readString(Paths.get(ktPath), java.nio.charset.StandardCharsets.UTF_8);
int k = src.indexOf("val PALETTE256_ARGB = intArrayOf(");
int start = k + "val PALETTE256_ARGB = intArrayOf(".length();
int end = src.indexOf(")", start);
List<Integer> vals = new ArrayList<>();
StringBuilder num = new StringBuilder();
for (char c : src.substring(start, end).toCharArray()) {
if (c == '-' || (c >= '0' && c <= '9')) num.append(c);
else if (num.length() > 0) { vals.add(Integer.parseInt(num.toString())); num.setLength(0); }
}
return vals.stream().mapToInt(Integer::intValue).toArray();
}
}