Equation -> Groth-Sahai statement conversion tool

[jdwhite48]

One of the primary issues in the literature and in my personal experience with using Groth-Sahai beyond a black-box manner is that it's a non-trivial (and at times tedious) process to apply the many properties of bilinear group arithmetic and its equipped pairing to encode each equation into the desired (A * Y) (X * B) (X * Γ Y) = t form that is expected of a Groth-Sahai statement. Especially in situations where one must prove about the satisfiability of many different equations or with lots of unique / unstructured variables, this could become a laborious-- if not impossible-- process trying to even encode the Groth-Sahai statement properly for the API to accept it.

And so, I think it would be incredibly useful to have some sort of tool that, given a human-readable list of equations to be satisfied, restructures the different kinds of equations into a format that is amenable to Groth-Sahai, and also auto-generates the necessary equations that can be plugged directly into the API.

(n.b. this would likely be such a massive undertaking even IF I could figure out how to do it. And so, I'm pre-emptively marking it as wontfix. I have no idea if I'll even get here, but I'll keep the issue open in case I or anyone else reading this finds inspiration to work on this)

[jdwhite48]

Custom-defining wrappers for different equations one might wish to prove about is a (maybe temporary, maybe permanent) workaround for this much more general and monolithic problem. Whether or not I or another contributor might want to generalize this functionality is still TBD.

[jdwhite48]

Looked more into the general strategy for doing this, and TL;DR automating the process of simplifying equations into a specific form is too much work (theoretically and esp. practically to both use and esp. to implement). for something that won't even provide that much benefit to most users of Groth-Sahai (easier to do by hand + with API for all but extremely complex structure of equations/statements). And so I'm dropping this proposed functionality from the repo.

Suppose that you have some generic equation q = r, and you want to reduce the terms in this equation into a Groth-Sahai equation s = t (where term s is in the normal form (A * Y) (X * B) (X * Γ Y), * denotes entry-wise pairings wrt bilinear map f, A,B are vectors of constant terms, and X,Y are vectors of variables, and term t is a constant). Then, I think an application of the Knuth-Bendix completion algorithm can solve this as follows:

Inputs (User):

• List of n equations (arbitrary bilinear group equations q_i = r_i)
  • Implicit: generate equations demonstrating properties of bilinear map(s) used, encoded as rewrite rules
• a (total) reduction ordering for these rules, which guides how to apply rewrite/reduction rules to arrive at normal forms described above
• List of n constant "targets" t_i corresponding to the "easy" part of the conversion of an arbitrary quadratic equation into a Groth-Sahai statement
  • Directs the algorithm to format the LHS of a Groth-Sahai equation, if target is consistent with a value that can be generated by an arbitrary equation above and applications of bilinear map properties.
• A maximum number of computational steps (or more concretely, time) before the algorithm forces termination with error

Execution:

• For end-user input, figure out an encoding of universal (for GS) rewrite rules for which all bilinear map and group properties are available, and the only normal form is a Groth-Sahai term of the form (A * Y) (X * B) (X * Γ Y) as described above (also allows adding identity elements if necessary; also, this would likely be difficult even if KBC implementation is a given, especially if KBC is defined with respect to word problems for abstract rewriting systems).
• Run KBC n times, once for each equation (or all as a single batch, I'm not sure).
• For end-user output, Strip out rewrite rules used in bilinear group equations (NOTE: since these might become incorporated, this entire approach might not even work), leaving only the n rewrite rules for deriving LHS of GS statement.

Outputs:

• a confluent term rewriting system (i.e. list of confluent rewrite-rules t_i' -> s_i') in which the KBC algorithm either:
  • reduces the q_i = r_i equations into rewrite rules of the GS form t_i -> s_i if possible, or
  • either fail early in reducing these rules in a confluent manner or continue forever if no such reduction to GS statement normal form exists (i.e. forcibly terminates after exceeding the max computation limit provided as input)

However, this would incur significant complexity in having to encode valid rewrite rules, implement KBC, checking for / proving about confluence, and/or learning an entirely new programming paradigm that facilitates me working with doing the above. Arguably it wouldn't even be that helpful for this specific application (since a user at the very least has to know what they want the "target" constant on the right should be but, understandably, is only too lazy to format the LHS correctly). Also, such a term-rewriting system for equations over bilinear groups definitely could find usage elsewhere as well, and need not be tied to Groth-Sahai.

For all of these reasons and more, I am shelving this issue indefinitely, and dedicating this repo to simply be a collection of wrapper for particular sets of equations, included as-needed. If anyone wants to build off this idea, feel free to do so in another repo (and reach out to me! I'm interested if this would work, and would greatly appreciate acknowledgement for the idea)