Bound the assembly stack size and fix its bytes/words confusion (scrutineer #2517)

[JasonGross]

Fixes scrutineer finding #2517 (duplicate of #2515).

The bug

When --asm-stack-size is not given, assembly_stack_size in src/Assembly/Equivalence.v infers the stack size from the hints file by summing the immediates of sub rsp, n / push / lea rsp, ... instructions. The result is an unbounded N; it is converted with N.to_nat (unary, since ExtrOcamlNatInt is not used) and then used as the number of stack placeholder cells to create (build_inputarray, build_merge_array_addresses, LoadArray). A two-line hints file containing sub rsp, 0x100000000 therefore makes the synthesis binary allocate billions of cells before it can report anything; with the assoc-list dag (linear insertion), it never finishes. An absurd explicit --asm-stack-size does the same.

Independently, the report's unit-confusion claim is correct: the inferred quantity is in bytes (push contributes 8, sub rsp, n contributes n, the System V red zone is 128), and --asm-stack-size is documented as "the number of bytes of stack", but the consumers (compute_stack_base = rsp - 8 * stack_size, compute_array_address strides by 8) treat it as a count of 64-bit words. Every check modeled [rsp - 8n, rsp) instead of [rsp - n, rsp): 8x the cells, and with the quadratic dag up to 64x the time. This over-approximation is sound (the extra cells are fresh symbols that are just loaded back at the end) but wasteful, and it would also silently accept assembly that touches memory well below its own frame plus the red zone.

The fix

• assembly_stack_size_words_of_bytes / assembly_stack_size_words round the byte count up to whole 64-bit words, and map_symex_asm now passes the word count to symex_asm_func. The statements of check_equivalence_correct and generate_assembly_of_hinted_expr_correct in src/Assembly/WithBedrock/Proofs.v are updated to match; their proofs needed no changes.
• New constant assembly_stack_size_max_bytes := 65536 and new error Stack_size_too_large (with Show case). map_symex_asm refuses any stack size above the bound before N.to_nat runs or anything is allocated. The --asm-stack-size help text states the bound.
• New negative tests: fiat-amd64/negative-tests/stack-size-too-large.asm (a sub rsp, 0x100000000 hints file) and an explicit --asm-stack-size 65537, both required to fail with the new error. They run via test-amd64-negative-files / only-test-amd64-negative-files, which are hooked into test-amd64-files* and only-test-amd64-files* (so CI's only-test-amd64-files-lite runs them).

Behaviour change for --asm-stack-size users (please read)

An explicit --asm-stack-size N used to model N words (8N bytes) because of the bug; it now models N bytes (rounded up to a multiple of 8), which is what the flag has always been documented to mean. Anyone who was passing a too-small number and relying on the accidental 8x is affected and must pass the real byte count. Nothing in this repository passes the flag (fiat-amd64/gentest.py, Makefile.examples), and all fiat-amd64 files verify with the inferred size.

Why 64 KiB, and why it also applies to explicit --asm-stack-size

• The largest sub rsp in fiat-amd64/**/*.asm is 1888 bytes (2016 with the red zone). 64 KiB is over 30x that.
• Measured with the rebuilt binary on curve25519 carry_mul: at the bound (--asm-stack-size 65536, i.e. 8192 words) the checker finishes in about 145 s using about 110 MB; at 2048 words it takes about 7.6 s. So the worst case an in-bound hostile input can cause is a couple of minutes, not a hang. (With the old binary, the same file's default inference already cost 256 cells; it now costs 16.)
• The bound applies to explicit values too: the cost is the same regardless of where the number came from, a clear error beats a multi-hour run, and a value above 64 KiB is almost certainly a units mistake. Raising it is a one-line change to assembly_stack_size_max_bytes, and the error message names that constant.

Alternatives considered: switching nat extraction to ExtrOcamlNatInt (does not fix the allocation of cells, and is a much bigger change); bounding only the inferred path (leaves the explicit-flag hang in place for no benefit); making the bound a CLI flag (more plumbing for a sanity limit nobody should need to move).

Verification

Done in a worktree against the installed coq-fiat-crypto-with-bedrock (Rocq 9.4+alpha), recompiling only the changed cone:

• coqc succeeded on: src/Assembly/Equivalence.v, src/Assembly/EquivalenceProofs.v (52 s), src/Assembly/WithBedrock/Semantics.v (HEAD version, differs from installed), src/Assembly/WithBedrock/SymbolicProofs.v (42 s), src/Assembly/WithBedrock/Proofs.v (133 s, no proof changes needed), src/BoundsPipeline.v, all seven src/PushButtonSynthesis/*.v that depend on it, src/CLI.v, src/StandaloneOCamlMain.v, and the extraction files for unsaturated_solinas, word_by_word_montgomery, solinas_reduction, dettman_multiplication.
• Rebuilt those four OCaml binaries by hand with the same ocamlfind ocamlopt command as Makefile.standalone.
• make -f Makefile.examples only-test-amd64-negative-files: both negative tests PASSED in about 2 s total. The hostile file now reports Stack size of 4294967424 bytes (...) exceeds the maximum supported stack size of 65536 bytes (assembly_stack_size_max_bytes); with the old installed binary the same file with the default inference does not terminate.
• make -f Makefile.examples -j8 only-test-amd64-files-lite SLOWEST_FIRST=1 (the CI target) with the rebuilt binaries: ALL 14 AMD64 ASM TESTS PASSED plus the 2 negative tests, 42 s wall.
• curve25519 carry_mul with a fiat-amd64 hints file and the default inferred size verifies in 0.46 s with the new binary (0.75 s with the old one).

Not verified:

• The full (non-lite) only-test-amd64-files run (p384/p434/p448/p521, the files with the largest frames) was still running when this PR was opened; I will update this description with the result.
• The src/Bedrock/** cone (bedrock2 standalone binaries) and the Haskell/JS extraction targets were not recompiled; they only consume the changed definitions through CLI.v and should be unaffected, but CI must confirm.
• No full make.

🤖 Generated with Claude Code

https://claude.ai/code/session_016Rbn2gww3MGhvrh52fNjpD