During occupation change I started following a course on Zero Knowledge Proofs. It helped to distract me from some boring routines, yes, but rather provided an answer on is there anything intellectually worthy in all that crypto shenanigans?

Yes, there is. What is labeled as Academic Crypto business is in fact usage of the popularity of blockchain and cryptocurrencies to promote and push forward the development of "traditional" Cryptography. In particular, the ZK cryptographic protocols with applications booming now through wide adoption of Ethereum L2 rollups.

The MOOC in question was in its first iteration when I started auditing it (although it was not the first online course made by the same authors). Submissions were to be made through Google Forms, and the grades were very generous. Anyways, the authors did great job explaining in details the architecture of the SOTA zk-SNARK systems. And there was also a practice lesson: a laboratory assignment meant to teach the usage of Circom language for proving the correctness (satisfiability) of arithmetic circuits.

It was fun but also quite hard to go through this assignment, because the paradigm of constraining circuits is different from the regular programming. One in fact writes 2 programs at once for every circuit, where only one of them can contain familiar arithmetic operators. The other is made of constraints, each of them being quadratic, linear or constant equations.

And while it wasn't complicated at first to fill the templates for the task - implementation of floating point numbers summation, in this case - the hardest part was to do so implementing a set of R1CS constraints for each circuit in a way that made the overall solution sound (all the importannt constraints are present).

Comparing to the walkthrough published by the course organizers this week, my solution was a mess). However even the authors admitted in their Discord channel that some of their own templates e.g. the CheckBitLength could be improved from the soundness point of view. Since they asked not to publish the solutions (and even the walkthrough video "expires" end of the week) I'll just leave the notes here on my own submission.

• CheckBitLength I implemented correctly - given that it is obviously a tweak of the Num2Bits already implemented in the template;

• RightShift is in principle correct, on the expected number of quadratic constraints too. The author's solution was better however;

• my LeftShift on the contrary was non sense. Formal tests pass but now I see it's not sound (and the tests won't show that). Also note the approach of (<value> - <test>) * (1 - skip_checks) quadratic constraint idiom;

• my error in MSNZB circuit is that I assumed somehow the correctness of some of the input signals, e.g. the "one-hot" vector to be always "one-hot". That's a mistake, probably, unless internally used Circom components establish needed constraints themselves;

• Normalize was only slightly different from the solution in the walkthrough. No surprise since it relies on the previously implemented components used along a known program flow path (a python example was given);

• finally, my LessThan was a disaster, only formally passing the test suit. I was low on time before the submission deadline and with some previous circuits relying on strange numbers of quadratic constraints... At least it was useful to watch the walkthrough afterwards and see how the signal passing was meant to be organized.

P.S.: One of the participants implemented the R1CS Solver that can help in checking soundness of a circom circuit.