Add code generation for Zig

[jedisct1]

This adds code generation for Zig, a compiled, safe programming language that can produce code for many targets, including WebAssembly.

Note that in Zig, types can have arbitrary sizes (u1, u2, u51, u2048), so we don't need to define any private types.

[JasonGross]

Thanks! Would you also add a .github/workflows/zig.yml, modeled after, e.g., the json.yml or go.yml file, to test the zig code on the CI? (Presumably you'll also need to add a step to install Zig.)

[JasonGross]

Also, if you have any comments or feedback on the experience of adding a new backend, have things that you think should be documented more, etc, I'd be happy to get such feedback.

[jedisct1]

Of course! A CI test has been added.

To avoid mixing two PRs, the generated files have the typo, but I'll regenerate them once the other PR is merged.

Adding a new backend was actually quite simple. Just one thing: there is a single instruction for changing the size of a value (Z_static_cast), no matter if it extends or reduces the size.

Type casts in Zig are safer than other currently supported languages. There are 3 ways to change the size of a value:

• @as() can only increase the size. Trying to reduce the size is a compile error. This operation is thus always safe.
• @truncate() can only shrink the size.
• @intCast() can increase or reduce the size, but in the second case, it can check at runtime that the operation preserves the numerical value, and immediately abort if bits would be lost.

@as should be called when we extend a value, and @truncate when we trim it. But I didn't get how to do it.

This is not that big of a deal, since @intCast() checks can be disabled on a per-function basis, but having a simple way to emit different code in both cases would be useful.

Ideally, most Z_land + Z_static_cast sequences could also be reduced to a single cast, since the target type can be of any size (@truncate(u51, x4)). But since these are two completely distinct opcodes, the way to do this is not obvious.

[JasonGross]

Of course! A CI test has been added.

Thanks! The CI has caught a bug:

/home/runner/work/fiat-crypto/fiat-crypto/fiat-zig/src/curve25519_32.zig:28:99: error: expected token ';', found 'Symbol'

Adding a new backend was actually quite simple.

Glad to hear it!

Just one thing: there is a single instruction for changing the size of a value (Z_static_cast), no matter if it extends or reduces the size.

Ah, I should be able to add an extra argument to Z_static_cast that says whether we're increasing the size or decreasing it. I'll open an issue to remind myself to do it.

Ideally, most Z_land + Z_static_cast sequences could also be reduced to a single cast, since the target type can be of any size (@truncate(u51, x4)). But since these are two completely distinct opcodes, the way to do this is not obvious.

This should not be done from the stringification code, which unfortunately remains unproven and should be as simple and direct a translation as possible. If it's really important to do this, I can look in to adding an extra rewriter pass keyed on an extra command-line argument to remove useless Z_lands.

[JasonGross]

This should be rebased and regenerated now that the other PR has been merged. Also, I forgot to request it before, please mark the .zig files as generated in .gitattributes in the way that the other generated files are marked. (I should make a contributing document with these steps.)

[jedisct1]

Hi Jason,

The changes have been rebased, the zig files have been regenerated, and the .gitattributes file has been updated.

[JasonGross]

Great, thanks!

[JasonGross]

One last request: Since none of us can vouch for the correctness of this code, are you okay with us adding you as the maintainer of this backend to the table I'm adding in #940?

And finally, it looks like you accidentally reverted a bump of coq-scripts; feel free to amend your commit to not change the coq-scripts submodule (you'll have to go into coq-scripts and check out the version that's at current master), or else I can just re-bump it after merging this.

[jedisct1]

Oops, I didn't notice the submodule was updated. The re-bump was amended.

And yes, I can take responsibility for maintaining the code. I'll be maintaining the code using it in the Zig standard library, so I can make sure it is correct, and keeps being updated along with new releases of the compiler.

[jedisct1]

Hi Jason,

Do you think this is ready to be merged, or is there anything else you'd like me to do?