inversion / divstep code broken?

[hannesm]

Dear all,

I've been using the C code generated by fiat-crypto 2a07751 (May 29th 2022) for a crypto library in OCaml. Now, due to some issue on a macOS machine, I wanted to update that code to a recent fiat-crypto commit (namely 1dc6b3a).

I noticed in my test suite that the inversion code (relying on divstep) changed in commit 822615f, and a commit from before that works fine, and after does not anymore.

So, I struggle: did the semantics of divstep change? Is the inversion_template being tested in CI?

If you like to take a look: this commit mirage/mirage-crypto@38adeb6 works fine (dune build tests/test_ec.exe && _build/default/tests/test_ec.exe); while this commit does not hannesm/mirage-crypto@cb578f1

Any help / clarification is highly appreciated... it may as well be that the issue is in my interfacing of the fiat-code.

[andres-erbsen]

I have just briefly looked into this, but I think you found a bug. Specifically removing the mask from
x74 = (fiat_p256_uint1)(x22 & 0x1); looks bad given fiat_p256_cmovznz_u64(&x22, x3, (arg3[0]), x12); and typedef unsigned char fiat_p256_uint1;. Overall (assuming I'm eyeing the right thing) the uint1-means-uint8 typedef is the part that is just wrong (casting to a "real" uint1 should truncate!); the redundant-and-removal optimization just unearthed the issue. There are no proofs about the (Coq->C/Rust/etc) pretty-printers, and I can't find any tests for divstep, so this would be exactly the kind of issue that we are not prepared against. My hunch is it's probably the right one.

I'll see how granular of a revert I can get in.

Given that you have tests for divstep, you could try out the C code printed using the more rigorous Bedrock2-based backend of fiat-crypto... https://github.com/mit-plv/fiat-crypto/blob/master/fiat-bedrock2/src/p256_64.c#L1669 would be the file for p256. But there's a number of reasons this backend wouldn't be a drop-in replacement, Bedrock2 being untyped and not having intrinsics are perhaps the most blatant examples. It does keep the required truncation, though, as proven.

[andres-erbsen]

I reverted the redundant-& optimization as a hotfix (ab4d8ac and c79cf60); I hope this gets you unstuck. Continued unsoundness of the IR-to-C printer will be tracked at #1606.

Thank you for the report! Please let us know if there's anything else we can help you with here.

[hannesm]

Thanks for your fix, this indeed works fine for me.

[JasonGross]

I reverted the redundant-& optimization as a hotfix (ab4d8ac and c79cf60);

We should probably parametrize the pass on a list of acceptable bitwidths to remove, then pass in [8; 16; 32; 64; 128] or something in BoundsPipeline