For this experiment I had it write directly.

I should add, part of the experiment was to test whether having variable names and (C style) types would help the LLM. For a task of this size (about 1.5 kLoC Rust, 3k insn asm) it was inconclusive, but for larger projects I suspect it would make a difference.

And the plan for symbolasm is to move past C style types into Rust style and maybe dependent typing, specifically to facilitate automated proofs.