fiat-html: make the argv string encoding a faithful round trip (scrutineer #2519)

[JasonGross]

Fixes scrutineer finding #2519 (Low, CWE-116): the argv string<->array encode/decode pair in fiat-html/main.js was not a faithful inverse, so a crafted ?argv=...&interactive link could display one command line in the text box while synthesising another.

The bug

splitUnescapedSpaces decoded the "Input String" text box by substituting U+0000/U+0001 as placeholders for \\ and \ and then dropping empty tokens; joinWithEscaping escaped neither placeholder. So ["a<U+0000>b"] re-decoded as ["a\\b"], ["a<U+0001>b"] as ["a b"], and ["a","","b"] as ["a","b"]. On load from a ?argv= link the text box is filled with joinWithEscaping(argv) while synthesis runs on the original argv, so the box and the executed command line diverged.

The fix

Only the two functions change, in place (fiat-html/main.js, +27/-10):

• splitUnescapedSpaces is now a character-by-character parser with no placeholder characters. Unescaped spaces separate arguments; \ , \\ and \" are a literal space, backslash and double quote; a bare "" token (delimited by spaces or the ends of the string) is the empty argument, which is the only new syntax. Any other backslash is kept literally, as before, so hand-typed input such as C:\path is unchanged.
• joinWithEscaping emits "" for an empty argument and escapes the quotes of an argument that is literally ""; quotes are otherwise left alone.

Since the pair is now an exact inverse, whatever the box shows decodes to exactly the argv that ran, whether the page was opened from a link or the arguments were typed by hand, and toggling between the string and JSON views never changes the arguments. No plumbing changes.

Verification (scratchpad only, nothing committed)

• A node test file that extracts the two functions from main.js by slicing the source and exercises them with hand-picked adversarial cases (empty args, U+0000/U+0001, backslashes, quotes, leading/trailing/multiple spaces, surrogate pairs), 20000 random arrays over [' ', '\\', '"', 'a', 'b', U+0000, U+0001], 20000 random legacy-only strings compared against the old decoder, and string->JSON->string stability: 8/8 pass on this branch, 6/8 fail on master.
• A jsdom harness loading the real fiat-crypto.html + file-input.js + main.js with a stubbed Worker: for ?argv=...&interactive links with an empty argument, a U+0000 in an argument, the README p256 link and a literal "" argument, the worker receives the URL argv and pressing Synthesize on the pre-filled box sends the same argv. On master the empty-argument case shows a b and would run ["a","b"] while the worker ran ["a","","b"], reproducing the finding. Typing x "" y\ z, toggling to the JSON view and back, synthesising, and reloading the permalink all give ["x","","y z"].
• node --check fiat-html/main.js is clean.
• Not tested in a real browser.

Possible follow-ups (deliberately not included here)

• With &inputType=json in the URL, updateInputType('json') runs the string decoder over the JSON text already in the box, so the box shows ["[\"a\",\"\",\"b\"]"] while the worker ran ["a","","b"]. This is the same display-vs-run divergence for the JSON view; the fix is to fill the box from the decoded array rather than the raw text.
• updatePermalink emits &inputType=&inputType=json, so a permalink from the JSON view always reopens in the string view.
• ?inputType= is interpolated into a CSS selector; a value like x"] throws and leaves the page blank.

🤖 Generated with Claude Code

https://claude.ai/code/session_016Rbn2gww3MGhvrh52fNjpD