In order to test the verification function we have to use the values of vk.json and proof.json by circom. To test this I will append our three factorial circuit example into the repo.
Problem
The problem now is how translate the values given by these .json files as G1 and G2 elements. Here is some clues that I have found:
Both G1 and G2 defined in Cardano follows Z-Cash encoding where they have a compress and uncompress form.
Serialization Format
From the ZCash BLS12-381 specification
Fq elements are encoded in big-endian form. They occupy 48 bytes in this form.
Fq2 elements are encoded in big-endian form, meaning that the Fq2 element c0 + c1 * u is represented by the Fq element c1 followed by the Fq element c0. This means Fq2 elements occupy 96 bytes in this form.
The group G1 uses Fq elements for coordinates. The group G2 uses Fq2 elements for coordinates.
G1 and G2 elements can be encoded in uncompressed form (the x-coordinate followed by the y-coordinate) or in compressed form (just the x-coordinate). G1 elements occupy 96 bytes in uncompressed form, and 48 bytes in compressed form. G2 elements occupy 192 bytes in uncompressed form, and 96 bytes in compressed form.
The most-significant three bits of a G1 or G2 encoding should be masked away before the coordinate(s) are interpreted. These bits are used to unambiguously represent the underlying element:
The most-significant three bits of a G1 or G2 encoding should be masked away before the coordinate(s) are interpreted. These bits are used to unambiguously represent the underlying element:
The most significant bit, when set, indicates that the point is in compressed form. Otherwise, the point is in uncompressed form.
The second-most significant bit indicates that the point is at infinity. If this bit is set, the remaining bits of the group element's encoding should be set to zero.
The third-most significant bit is set if (and only if) this point is in compressed form and it is not the point at infinity and its y-coordinate is the lexicographically largest of the two associated with the encoded x-coordinate.
Some findings and conclusions we have talked about this:
Strictly speaking, the Plutus VM doesn't recognize constructions PlutusData or lists with uncompressed points, only with compressed points (bytearrays). Although you can define data with uncompressed points in the source code, Aiken will do the transformation under the hood now given this commit
Once you transform the decimal coordinates of x-coordinate given by snarkjs to hexadecimal, you must alter the 3 most significant bytes (at the "left" of the bytearray since its Big-Endian). The first one means a compressed point; the second will explicit if its a point to infinty (in which case the rest of bits are 0); And the third explicit wether you use the maximum or minimum y-coordinate associated with the x-coordinate.
The arrays in both cases it will always start with a "8", "9", "a" or "b".
Anything to add @jmagan @ajuggler before closing the issue?
Context
In order to test the verification function we have to use the values of vk.json and proof.json by circom. To test this I will append our three factorial circuit example into the repo.
Problem
The problem now is how translate the values given by these .json files as G1 and G2 elements. Here is some clues that I have found:
Reference-1: https://github.com/supranational/blst#serialization-format Reference-2: https://ci.iog.io/build/1230997/download/1/plutus-core-specification.pdf
In aiken the definition of the uncompress G1 & G2 elements goes like this:
One can see more info about it in this in this PR: https://github.com/aiken-lang/stdlib/pull/79/files