Verification method and evidence grades
How we produce the evidence in this section, which claims we executed and which we inferred, the tools we use, and the two traps that produced wrong answers.
This page explains how we get our results — and what the method can't show. Every request page separates measurements from inference; this page defines that separation.
Evidence grades
We use three grades, and each request page states its grade.
| Grade | Meaning |
|---|---|
| Executed | We called the function and recorded the result |
| Observed | We watched the client behave, and we measured the behaviour |
| Inferred | We read the code and concluded. We did not run it |
An executed claim is the strongest. Six of our file-system claims are executed. The key-label claim is observed and partly inferred, and UR-08 says so on the page.
How we execute a shipped function
The path helpers are pure — no game state, no initialised UI — so we can call them from a cold instance.
Add an export
Append an export entry for the target function to the module. This changes the export section only.
Instantiate
Load the module in Node with stub imports. Most imports can return 0.
Call
Call the function with prepared arguments in linear memory. Read the result back from memory.
This method proved UR-01, UR-03, UR-04, and UR-05 directly; for
UR-05 we ran six inputs on build 38797 and recorded all six results.
We use the same method in reverse for UR-02: driving the derived forwarders
against a fake file system and comparing against the real bridge source.
How we observe live behaviour
For UR-06 we captured the syscall traffic of a save and a rename on a live
client. The captured flag value 32834 is the evidence.
For UR-09 we measured the gap between the cursor hide and the new cursor,
three times, with the pointer held still.
For UR-10 we read the peak heap value from three crash sessions on three
machines, and the compiled-in cap from the artifact the client downloaded. The
abort text in that request is the client's own, read off the crash view of a
player's machine — it never enters a diagnostics export, which carries only a
reason category and a non-text fingerprint. The growth curve comes from a
fourth session that did not crash: our host samples the heap size every two
seconds and records each rise, so a session's staircase is the sequence of
those events.
Tools
| Tool | Purpose |
|---|---|
| A full instruction decoder | Decodes every function body. It decoded 17,600 of 17,600 functions on build 38,771 with no failures |
| A symbol generator | Attributes functions to translation units, using the 219 import names, the 44 export names, and 850 source paths in the data section |
| An anchor probe | Checks which assert strings still identify exactly one function on a new build |
The tools are published in the project repository, and we can supply the scripts behind any result in this section.
Two traps that produced wrong answers
LLVM writes relocatable constants as zero-padded, non-canonical LEB128. For
example, i32.const 0x102820 is 41 a0 d0 c0 80 00.
A byte search for the canonical encoding finds nothing, and it finds nothing silently. Decode the instructions instead of matching bytes. This cost us time twice.
How we derived the double-click channel twice
We established UR-07 two times,
independently: once forward, from the Emscripten input callbacks to FrMouse,
and once backward, from the FLAG_DBL_CLICK assert to the input record. Both
derivations produced the same chain and the same missing byte, and every
function index, offset, and constant came from a full instruction decode.
We also recorded two supporting negatives: the import list holds no
emscripten_set_dblclick_callback, and the strings dblclick, clickCount,
and DblClick occur nowhere in the binary.
What our method cannot show
- We cannot call a function that needs an initialised UI. The label render
in
UR-08is one example; that page states the boundary. - We cannot prove a memory address. An address has no shape in the module. We measure it on a running client, and the measurement holds for that build only.
- We cannot see the source. Every source attribution in this section comes from an assert string. When a translation unit ships no assert, we cannot name it.
- We have one client build at a time. We can prove that a check refuses a changed module. We cannot prove that a locator survives the next build until the next build exists.
How to check any claim yourself
Every request page has a reproduction procedure. The procedures need a stock client — no part of our host, and no modification of the module, except where a page says otherwise.
If a claim in this section is wrong, tell us. We'll correct the page and say what we got wrong.