<k​ayabanerve:matrix.org> For the past couple of weeks, quotes were solicited from the following parties (in order of received SoW):

<k​ayabanerve:matrix.org> - Least Authority: Review of Eagen's commentary on correctness and the specified R1CS gadget. 55,960 EUR + 31,541 EUR if paid in a timely fashion.

<k​ayabanerve:matrix.org> - Veridise: Review of Eagen's commentary, an explicit proof or counterexample of Eagen's work, and review correct transformation into a R1CS gadget. $250 an hour, across 8-24 hours, with +$4,000 upon said proof or counterexample.

<k​ayabanerve:matrix.org> - Trail of Bits: Review of Eagen's commentary on correctness and the specified R1CS gadget. $50,000.

<k​ayabanerve:matrix.org> - Cypher Stack: Review of Eagen's commentary on correctness and the specified R1CS gadget. 210 XMR.

<k​ayabanerve:matrix.org> - Quarkslab: Review of Eagen's commentary on correctness and the specified R1CS gadget. $48,500.

<k​ayabanerve:matrix.org> - Brandon Goodell: A formal write-up and review of Eagen's commentary on correctness and the specified R1CS gadget, with a proof if possible. $185 hourly, 130-150 hours ($24050 - $27750).

<k​ayabanerve:matrix.org> We also solicited a SoW from JP Aumasson, yet they aren't actively working as an auditor.

<k​ayabanerve:matrix.org> Believing the researcher at Veridise competent (having been involved with a variety of academic works on fields), and given their cost being significantly less than the other options, jberman and mine's endorsement at this time is Veridise. When asked if they truly believe the work feasible in that amount of time, they do believe it amenable (though it may end up requiring an exte<clipped message

<k​ayabanerve:matrix.org> nsion, as anything may, see how the recent GBPs work risked being inconclusive) and a payment is conditional to a result in order to create the proper incentive structure and preserve value upon an inconclusive result.

<k​ayabanerve:matrix.org> Depending on how their work goes, we'd ideally move on to contracting another group for review of their output (a couple candidates standing out as preferred). This is expected to be discussed at the next MRL meeting yet is posted here now for review ahead of time.

<k​ayabanerve:matrix.org> Also, Veridise quoted payment via a wire transfer or USDC/USDT. Payment would be handled through MAGIC who has volunteered their facilitation. It's partially up front, partially within the conclusion of the scope of work. I'd call for the full amount to be transferred to MAGIC at time of consensus as necessary to secure the USD valuation. cc sgp_ if they'd like to further comment.

<r​euben:firo.org> Wow Veridise quote is max 10k?

<k​ayabanerve:matrix.org> There do be a reason they're endorsed.

Is it not worth getting two independent reviews done, for comparison?

as opposed to a peer review of one output. I understand there will be redundancy with concurrent reviewing, but i think it a more robust strategy (though could be wrong). It's also what we did with RandomX, iirc.

<3​21bob321:monero.social> Double spend

midipoet this is true. example rekt.news/raft-rekt "Raft had been extensively audited by four organisations, including > Trail of Bits < and a Hats Finance contest."

We actually funded three concurrent audits for RandomX

And there was a fourth done also, for comparison (but paid for by Arweave it seems).

<g​ingeropolous:monero.social> i think those were done when the code was ready? is the current effort at the same place? or is this like a preliminary 3rd party review of the underlying whatsits? to me it seems the second, based on this specificity "Review of Eagen's commentary on correctness and the specified R1CS gadget."

<k​ayabanerve:monero.social> midipoet: We can obtain two reviews of the underlying which say the same thing, or we can get one review and have that reviewed. The distinction is that instead of independently coming to stronger commentary which isn't yet strong enough, we can achieve stronger commentary, than secondary reviee _and_ the sufficiently strong comments.

<k​ayabanerve:monero.social> Like, literally, two independent proofs of this does not help us. Any proof *with peer review* does.

<r​ucknium:monero.social> kayabanerve: Thank you for doing the work to get these quotes! "Eagen's commentary" is eprint.iacr.org/2022/596 and R1CS is what? Is it this? monero-project/research-lab #116

<k​ayabanerve:monero.social> If we were not potentially soliciting proofs, this would not be necessary except for distinct concerns of it being financially irresponsible. If one party tells us it's completely insecure and broken, do not touch, we don't need to hear from a second party we gave $30k and a month of time the exact same just a few days after the first party reports that.

<k​ayabanerve:monero.social> It's the correctness section of that paper for the first numbered equation.

<k​ayabanerve:monero.social> No. That issue has nothing to do with this. At all.

<k​ayabanerve:monero.social> It's the R1CS gadget specified in the FCMP++ paper.

<k​ayabanerve:monero.social> *the R1CS gadget specified for proving discrete logarithms

<r​ucknium:monero.social> I ctrl+F for r1cs in the FCMP++ and didn't see any matches

<k​ayabanerve:monero.social> Said gadget is an R1CS evaluation of Eagen's equation 1 (and implied protocol). If the math follows, this specification is what we'd actually implement in-circuit.

<k​ayabanerve:monero.social> Section 4.3 is a R1CS constraint system.

<k​ayabanerve:monero.social> The following gadgets are R1CS gadgets, 4.4.2 being the one relevant here.

<r​ucknium:monero.social> Could you make a gist explaining exactly what's proposed to be reviewed? You can point to the sections in Eagan's paper and your own.

<r​ucknium:monero.social> And for the quote-proposals that will attempt to write proofs, which proposition(s) will attempt to be proven?

<r​ucknium:monero.social> Attempt to write proofs or create counterexample(s), I mean.

<r​ucknium:monero.social> About the options to (1) have one proof written plus the proof reviewed compared to (2) two proofs written by independent entities: Mathematics and code are different. IMHO, having a second independent proof attempt in (2) doesn't have zero value, but it is not as good as reviewing a single proof in (1).

<k​ayabanerve:monero.social> 1) It depends on which is being discussed. It's always Eagen's... 3.3.1? (the section on correctness for equation 1) and the R1CS gadget.

<k​ayabanerve:monero.social> 2) The statement Eagen proves for in statement 1 is effectively that points sum to 0. I formalized this in github.com/kayabaNerve/fcmp-ringct/blob/divisor-paper/divisors.pdf. It leaves a spot for a proof premised on witness extraction. Not all proofs proposed are so premised, but the proof discussion is functionally equivalent as far as we're concerned.

<k​ayabanerve:monero.social> That document is a summary of the background, a formalized protocol (not simply an equation), and the R1CS gadget. Accordingly, it is the best reference.

<k​ayabanerve:monero.social> Please note it came after some proposals were solicited so some proposals are scoped to the background and the gadget included in the paper, not the paper itself.

<r​ucknium:monero.social> Thank you. Could you create a gist of the quotes summary you gave above and the expected scope of work to provide a reference to everything in one place? Especially since your divisors.pdf is in a separate git branch of `fcmp-ringct`.

<k​ayabanerve:monero.social> When I'm around next 👍

<r​ucknium:monero.social> Thanks a bunch :D

<k​ayabanerve:monero.social> Of course