Did you have it go directly to asm or emit the assembly from the Rust toolchain and then contract that? For small stuff, I have been having it write directly, or larger pieces I am having better results via contractions.

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.