15:01:16 MRL meeting in this room in two hours. 15:02:08 Stay hydrated. Will probably be a long meeting. 15:21:35 I propose that the "1. Greetings" get replaced by "1. Water check" 16:42:45 Hi all! I'm Ben Sepanski, CSO from Veridise. In light of the upcoming discussion, we wanted to share Veridise's perspective on FCMP++ and SLVer bullet. 16:42:47 Since SLVer Bullet was updated based on the attached concerns (after we shared them directly) and announced before we heard back from Cypher Stack, we wanted to go ahead and share them publicly in case they are found useful by the Monero community or any future reviewers planning to create/analyze security proofs for SLVer Bullet. While we do not intend to perform further review, based on a brief pass we believe that neither of the two most serious issues raised were addressed by the update: 16:42:51 * The use of explicit curve addition formulas in the derivation of the verification equations results in relations that do not hold at the function field level (and are not equivalent to the expressions proposed by Eagen as claimed). See, for example, the SAGE script above, in which the original equations match the expected expression computed using SAGE's built-in functions, but SLVer bullet does not. As mentioned, we do not have capacity at this point to perform further reviews of SLVer Bullet, but the underlying issue of applying derivatives to an expression which holds over only a subset of the curve is still present 16:42:55 * The soundness argument contains a flaw in the use of Schwartz-Zippel, which also has not been fixed. SLVer Bullet’s soundness argument (Theorem 3.3.7) relies upon "Sage code 2 (see [Sla25]) giving statistical evidence of that the two cases result in the same distribution of roots, enabling our application of Schwartz-Zippel.” This does not constitute a proof and cannot provi de the basis for soundness of a cryptographic argument 16:42:59 To avoid multiple rounds of back-and-forth, we plan to continue work along the original line of reasoning based on the ideas of Eagen and implementation by Kayaba, and will share here if we have more updates 16:43:01 As mentioned in the first response, we reiterate our commitment to be actively involved in any constructive endeavour to ensure the correctness of the proofs, the clarity and precision of its exposition and the security of the scheme based on it, and hope this is helpful for any future decision-making. As always, we remain open to any further questions or concerns! 16:43:03 log_deriv.ipynb 16:43:05 https://matrix.monero.social/_matrix/media/v1/download/matrix.org/mrIQjbCrDTXpPLilgKjXsdwb 16:43:07 https://matrix.monero.social/_matrix/media/v1/download/matrix.org/ilabQZKNKVDxZrXZAbQvWROw 16:43:09 https://matrix.monero.social/_matrix/media/v1/download/matrix.org/gNUdNJDsKZsnxOmnriExRNLj 16:47:22 ben_sepanski: Welcome! Thank you for sharing. 16:58:42 For the first point, our new numerical values may be found on page 16 and 23, so the provided Sage code is no longer relevant, as it applies to the prior version. For the second, the Schwartz-Zippel issue HAS been addressed, on page 13. Our code was merely intended to provide, as we state, *statistical* numerical evidence, so was never intended to constitute a proof. It seems as i f there are misunderstandings between what we intended and what you have read (no claims as to who is "at fault" here, but we will clarify these issues in future versions). Veridise, we do appreciate your review, and thank you for helping to make Monero better, which is ultimately what we all want! ❤️ 17:00:33 Meeting time! https://github.com/monero-project/meta/issues/1244 17:00:42 1) Greetings (water check). 17:00:55 Hi 17:00:58 hello 17:01:03 glass half full 17:01:04 ji 17:01:05 hola 17:01:16 Hello! Are there leaks? 17:01:22 *hi 17:01:23 hi 17:01:25 hello (hydration check) 17:01:27 Howdy 17:01:37 hi 17:01:37 👋 17:01:54 *waves* 17:02:27 seas 17:02:29 2) Updates. What is everyone working on? 17:03:00 me: Analysis supporting changes to the DNS ban list: https://github.com/monero-project/meta/issues/1242 . Evaluated feasibility of setting up "honeypot(s)" to learn more about the infrastructure of the spy node network (seems feasible so far). Guided ditatompel to add MRL/DNS ban list columns to his table of remote nodes: https://github.com/ditatompel/xmr-remote-nodes/issues/191 https://xmr.ditatompel.com/remote-nodes 17:03:08 me: got lwsf into monero_c. but the bindings need to be re-worked and the build process is problematic 17:04:30 me: steering these bots to make this monerosim work 17:05:27 3) [SLVer Bullet: Straight Line Verification for Bulletproofs](https://github.com/cypherstack/silver-bullet). [Cypher Stack review of divisors for FCMP](https://github.com/cypherstack/divisor_deep_dive). 17:05:43 me: drafted a proposed spec for PoW-enabled relay "PoWER" (https://github.com/monero-project/research-lab/issues/133), handled compiler warnings for FCMP++/carrot with some help from jeffro too, set up core tests testing constructing a FCMP++/Carrot tx spending from a pre-rct tx, tests went smooth 17:06:46 I would like a summary and bottom line of what has happened since the SLVer Bullet paper was first released. 17:07:32 I think it would be best to hear from CS what they did, and then kayaba or I can summarize what that means for Monero and the implementation 17:07:35 We put out an update yesterday with extensive changes taking Veridise's review and annotations into account. 17:07:51 We also were able to prove that our verification equations are just simplifications/reductions of Bassa's/Eagen's 17:08:07 Me: getting very close to a first working version of hot/cold wallet implementation for Carrot/FCMP++. Importing/exporting received outputs works, creating transaction proposals works, signing works, and finalizing FCMPs and BP+s on the hot side works. It is completely backwards compatible up until when the FCMP++ fork activates, and shouldn't require much downstream reworking. Th e RPC interface is *almost* unchanged, except for a quirk where b/c of detached FCMP++ signing, the cold wallet doesn't know TXIDs of signed transactions, but that's how tx private keys are fetched in the RPC interface. The hot/cold protocol, as implemented, also supports "stateless" hot/cold interaction, cold-initiated transaction proposals, reduced overhead when hot wallets "rem ember" tx proposals, and Carrot-derived-key wallets in the future 17:08:11 In a sense, criticisms leveled by one of us toward the other or vice versa are superficial 17:08:35 we were able to improve soundness bounds and little stuff like that, and improve the arithmetical efficiency of our version over the previous 17:09:23 we present some statistical* evidence in the paper that our arguments are equivalent to Bassa's and we also provide a calculus-based explanation of why 17:09:56 we still have some issues we are currently addressing which revolve around kayaba's code 17:10:06 but other than that, "mysteries are solved," so to speak 17:10:30 Shall I step in with my perspective now? 17:10:48 don't ask, just do :) 17:10:50 Always <3 17:10:52 I know sgp_ wanted to first hear from CS. 17:11:58 Veridise and Cypher Stack, as of a week ago, disagreed with each other's work. Currently, Cypher Stack is signing off on Veridise's work. We have already done the implementation for and audited Veridise's work. That reduces, albeit incredibly so, all of the work of Cypher Stack to one, very long, and with many adjacent threads, review of Veridise's work which has come back with approval. 17:12:08 *is now signing off on 17:13:16 to be more specific, it might be best to say "cypher stack believes that eagan's scheme is secure to use" 17:13:45 Our initial contract was to look over Bassa's / Eagen's stuff. We found it unconvincing, mostly because lack of background, proofs, and skipping over several things we deemed important. Reverse engineering that work to get it to the level of mathematical rigor we were comfortable with was taking quite some time and MRL was putting pressure on us to deliver quick. 17:13:47 Given the time constraints, we gave a thumbs down, even though our guts told us that it would probably work out correctly. We just didn't have the time to do said rigor. 17:13:49 We decided to take our own stab at it and made SLVer Bullet. During this current Stack Attack we have shown to our own satisfaction that our methods are equivalent to Veridise's. In so doing, we have fulfilled our original goal of giving a thumbs up or not do Eagen's / Bassa's work, though in a roundabout method. 17:13:51 Right, sorry. Signing off on the result, if not necessarily the methodology and existing work. 17:14:46 The only reasons to discuss Silver Bullet would be if we believed it more efficient to Monero in a way worthwhile of time and effort to migrate (non-trivial). Given how marginal any performance benefit would be _within our context_, I can not endorse investing that effort. That means, for the purposes of our discussions, even if Silver Bullet is an amazing artifact representing mo nths of works, we can simply add it to a list of texts in our library for this line item and move on. 17:15:18 Note the Silver Bullet paper proposes its own contexts/use-cases, and I am thankful to Cypher Stack for their self-organization and investment of their effort to promote Monero's security. 17:15:20 Given the above, Cypher Stack is, at this point, confident is saying that either Eagen / Bassa's work, or SLVer Bullet is fit for use in Monero. 17:15:21 Our continued work on SLVer Bullet has yielded several optimizations that we think would help Monero somewhat (though not massively), so we (obviously biased) think it may be worth it to look at the speed ups for SLVer Bullet and see if they would be worth the time to recode. And if not, using Eagen / Bassa's stuff is fine. 17:15:23 _very_ thankful 17:15:49 <3 17:15:52 marginal improvements, in Monero's specific context, are ~1% right kayabanerve ? It may be more efficient in other contexts 17:15:53 Within the context of the FCMP, each invocation of the current proof is _7_ rows in the IPA. 17:16:54 If that was decreased to five, we'd save ~8% of the proof. As the proof is padded to a power of two, we only observe literal performance benefits w.r.t. the summary MSM if we improve performance by 50%. 17:17:41 I'd find five a notable result, yet that doesn't change yes, it's of no effect when we're already at such a small constant. 17:18:24 We can argue the performance of linear constraints, which don't impact the size of the MSM, yet that's the point: they don't impact the size of the MSM. They're so relatively cheap I didn't even find them worth measuring the performance impact of. 17:19:10 Are these numbers for verification time or proving time? 17:19:32 inb4 even 1% is welcome on the verification side 17:19:39 And as per the witness size within the dedicated commitments, the one other metric this category of proof could improve in, I believe Cypher Stack agrees the current work is optimal. We currently represent a 256-bit scalar multiplication using: 256 field elements correlating to bits _and_ a 256-degree witness (SB's MakeWitness function) which has up to 256 roots. 17:19:49 > we only observe literal performance benefits w.r.t. the summary MSM if we improve performance by 50% 17:20:07 we *did* improve our proof size over the previous version 17:21:12 surae: Communication of the Silver Bullet proof, for a 256-bit scalar multiplication, requires the scalar itself _and_ a witness polynomial with at least 256 elements, correct? 17:21:17 SyntheticBird thank you, we definitely beat 1% 17:21:35 I understand the prover builds the proof from there. I just want to set the base fact of how that communication is still required. 17:22:31 K, I immediately want to clarify this: Cypher Stack did not build nor propose a proof for usage within a Bulletproof. If we were to adopt Silver Bullet, we'd have to apply the same techniques as seen with the existing work to execute it within a Bulletproof. 17:22:53 The performance benefits claimed, to proof size, proving, and verification, become negligible within the context Monero currently wants to use this proof in _AFAIK_. 17:23:22 In the contexts Cypher Stack proposed, designed, and built, their proof for: Oh yes, much more efficient. No disagreement. 17:23:33 *Within* a Bulletproof, we present divisors *applied to* Bulletproof 17:23:42 _Within_ a Bulletproof, we present divisors _applied to_ Bulletproofs 17:23:43 kayabanerve @kayabanerve:matrix.org: correct 17:23:46 re: proof size 17:24:02 not including a few extra field elements 17:24:23 surae: Right. With the current proof, the only elements we explicitly commit to in Pedersen Vector Commitments is the scalar itself (decomposed) and the 256-element witness polynomial. 17:24:36 If both proofs have that (the statement and the witness polynomial), there is no room for improvement there. 17:25:17 The only improvement, _within our context_, is with regards to the IPA rows (currently a constant `7` which means any improvements are marginal) or with regards to the linear constraints (a negligible part of our performance). 17:26:04 I am not trying to bash Silver Bullet, which proposed new contexts and made great efforts on their efficiency. I just want to keep the discussion focused to our current context due to the amount of discussion we've had on it already, ideally culminating here and now. Introducing yet more doesn't help wrap this up. 17:26:31 But the new contexts proposed are worthy of review and consideration, and I do believe CS deserves acknowledgement for them: I am just asking not right now. 17:28:58 Because Veridise and Cypher Stack agree on the current implementation's definition, the only note is one question I raised with Cypher Stack recently. The Silver Bullet paper defines a `line` function, while my implementation has our own `line` function. The two are distinct. This would imply my proofs... math differently, and yet they are accepted by the verifiers I've defined an d tested with. If my proofs are valid, yet their math is different, why are they valid? 17:29:38 That's something we're trying to address right now! 17:30:04 I've asked Cypher Stack for an answer (of which they are not obligated to give, of course), but I believe they've been generous enough to work on to at least some degree. if this one 'discrepancy' is resolved with Cypher Stack, I see no reason not to consider the theory accepted and move on to discussing a second audit of the implementation: as-is. 17:30:25 (including potentially not obtaining a second audit, I'm just noting where the discussion would shift) 17:30:31 I am confused by the current status of the objections raised by ben_sepanski at Veridise: 1) [Something] does not hold at the function field level. 2) Rigor of proof using Schwartz-Zippel lemma. 17:30:31 I think Cypher Stack thinks it has adequately responded to those objections in the latest version. Does Veridise still think the objections are valid, or not, or has Veridise not yet (and may never) looked at Cypher Stack's responses? 17:32:18 Rucknium: While I'd be happy to let Ben clarify their own position, as I do not want to speak for them, I also don't wish to expect their answer nor demand their time. Their review of Silver Bullet was voluntary. My discussion short-circuited if Veridise agreed with Cypher Stack by nothing both parties agreed on the results worked on by Veridise. That means we don't _need_ Silver Bullet to be agreed upon, as we aren't implementing it. 17:32:52 We, to the best of our knowledge, have addressed every "category red" comment that they provided to us, as well as most of the "category orange" comments 17:33:50 So we argue that their two big points are not problematic for our case 17:33:51 So you could say that all this brings cryptography forward, but does not immediately influence us on the way to the first FCMP++ hardfork? 17:33:58 So we argue that their two big points are not problematic 17:33:59 Though we can also shift back to discussions on hiring Veridise for _mutual agreement_, hiring a third entity to review Veridise's work (with Silver Bullet provided as an auxilliary text), or continuing work on a unified publication regarding divisors _as oriented by Veridise_ to encourage further review. As that last discussion occurs, I'll note I believe Cypher Stack are already continuing with their publication, which should cause any inherent/natural review on their claims (including the claims of equivalency). 17:34:10 Freeman's response here to their response today 17:34:11 Thank you very much to Veridise for reviewing the work 😁 17:34:22 On (2), we do not believe the Schwartz-Zippel lemma (as written in either version of SLVer Bullet) can be applied. This is essentially because standard Schwartz-Zippel requires sampling variables [x,y] independently. When sampling points on an elliptic curve, the curve equation enforces a relation between x and y 17:34:23 On (1), we have not had time to look in detail at the updated derivations since our initial comments. It sounds like the updated equations match Eagen's, in which case they may be correct 17:35:27 kayabanerve: can you clarify the current primary blocker with the implementation? That's the most important thing for everyone to understand in the moment 17:35:30 Thank you, ben_sepanski 17:35:38 We can continue this part of the conversation in the Research Lounge? 17:35:40 The dependency between coefficients vs roots will be equivalent, by Vieta's formula. And our statistical evidence supports our viewpoint 17:36:48 #monero-research-lounge:monero.social 17:37:24 sgp_: Cypher Stack believes their work equivalent, therefore proving the validity of Veridise's work in their own method. Despite this, Cypher Stack's work suggests my work shouldn't work. As my work appears to work, the _implied result_ of Cypher Stack's _claimed result_ does not _immediately_ hold. I believe this should be fully understood before we continue with the _claimed re sult_, which is that Cypher Stack agrees with the current protocol because it can be proven equivalent to their own work. 17:37:38 "based on a brief pass we believe that neither of the two most serious issues raised were addressed by the update" vs "we have not had time to look in detail at the updated derivations since our initial comments. " 17:38:01 "based on a brief pass we believe that neither of the two most serious issues raised were addressed by the update" vs "we have not had time to look in detail at the updated derivations since our initial comments. " 😕 17:38:03 If I understand correctly, the two Veridise objections affect SLVer Bullet and not Eagen's original work, right? (I guess this is obvious now, but I want to make sure I have this clear.) Or do they affect the claimed proof in the SLVer Bullet paper that SLVer Bullet and Eagen's work is in some way equivalent? 17:38:08 Freeman Slaughter: can you please leave this? In the context of Monero we don't care right now 17:40:41 Rucknium: Correct. Cypher Stack believe Veridise's work is correct because their own work can be argued a method of proving Veridise's work. Veridise believes Cypher Stack's work has faults, and is therefore insufficient as a proof to this claim, but it doesn't change Veridise's work is only invalid _with both parties being wrong_. 17:40:58 This means we do have two independent organizations claiming the security of this result. 17:41:25 Previously, Cypher Stack said that the calculus work in Eagen's paper was "incorrect". How can this be? Was it 1) The calculus was correct, after all, 2) Cypher Stack found another way around the problem that didn't involve the "incorrect" calculus, or 3) Something else? 17:42:32 Though I still want to understand why the 'implied result' is not immediately understood, which of course Cypher Stack has said they're working on (much to my appreciation). 17:44:56 We always argued that Veridise *could* be correct, just that we were not convinced by their proofs. An unjustified proof can never be correct, because it relies on something whose veracity is not supported. The calculus was correct, in a consequentialist sense, but their proofs were confusing enough for us that we were forced to rederive them from scratch (which we only recently f inished to a level that we found sufficient) 17:46:50 From what I understand today, I would prefer that a third firm confirm the correctness or one or both of Veridise's and/or Cypher Stack's claimed proofs of the soundness of Eagen's divisors. 17:47:01 Rucknium, you're referring to the fact that in a previous MRL meeting, I stated that the calculus was incorrect. 17:47:03 This was because Brandon had said that Eagen had incorrectly applied the chain rule. The incorrectness comes from the fact that the use of it in that context was not justified. 17:47:05 For instance, their usage of the chain rule was not justified, in our view. So any application of it is "incorrect" until that step is justified 17:47:38 fwiw, I would support getting a third firm involved to look things over. 17:47:44 Rucknium: another review of the Eagan technique may still be warranted, yes 17:47:49 We can move forward with testnets and things in the meantime. 17:47:59 But these two firms are currently in agreement with the Eagan scheme being secure 17:48:01 Rucknium: You understand we currently have both research outfits agree the currently defined proof is secure, with independent methodologies, correct? 17:48:26 They don't agree on the same mathematical proof. 17:48:36 The fact they disagree on their methodologies does not shift _both must be wrong_ for the proof to be wrong. 17:48:37 That isn't what I expected. 17:48:56 They disagree on the _security proofs_ for the proof. 17:48:59 I expected CS to agree that Veridise's original proof was correct. 17:49:07 They both agree the proof has the desired mathematic effects w.r.t. elliptic curves. 17:49:19 Incorrect. They didn't make security proofs to disgree with. :P 17:49:21 They do agree the proof is correct. They disagree the arguments for it, at the time, were convincing. 17:49:29 they got to the same result with different work, which wasn't the simplest path but it still a valid option 17:49:44 CS wrote a new proof. 17:49:47 Diego Salazar: While a joking comment, it makes no difference to this discussion. 17:49:57 if budget allows, a third review could be commissioned, but it's not really _strictly_ necessary 17:50:16 Rucknium: Which is why we currently have two independent groups, with two independent methodologies, agreeing the defined proof is built on sound theory. 17:50:26 Hmm, doesn't the mountain of material to potentially review grow all the time? 17:50:50 If I understand correctly, the two firms disagree that the other's proof is fully valid. 17:50:53 Which is why I'd prefer to discuss using the budget on a second audit, before discussing a third review of the theory, with the emphasis being I'd like to move forward. 17:50:54 Now already two different proofs, if I understand correctly 17:50:59 a third reviewer might in theory make yet a third route to also support security 17:51:09 :) 17:51:16 (all of this assuming the 'implied result' thing gets circled back on, which I expect and believe will occur) 17:51:33 Do we know 51 qualified research outfits eligible to participate in a ranked-choice vote? 17:51:51 Is ZK-Security no longer available? 17:51:55 Rucknium: The other's arguments for why the proof is valid. They agree on the proof. 17:52:00 Ultimately, any disagreement with our work is a disagreement with Eagen's work, since we've shown them to be equivalent 17:52:06 Rucknium: The other's arguments for why the proof is valid. They agree on the proof we would implement in _some context_. 17:52:26 The proof != the security proofs, as I keep trying to iterate. 17:52:28 AFAIK, Veridise isn't sure that the equivalency holds. 17:52:37 Diego Salazar: I was making a joke on ensuring qualified review. 17:52:38 Ultimately, any disagreement with our work is a disagreement with Eagen's work, since we've shown them (the verification equations) to be equivalent 17:52:49 but Veridise independently supports the Eagan scheme 17:53:15 I would advocate for a 3rd independent review before mainnet, but prioritize tasks that move forward toward mainnet 17:53:17 both groups agree Eagan's scheme is secure 17:53:19 Why did cryptographers name something "proof" when that term was already taken? 🤔 17:53:26 Correct. So the actual summation is that: 17:53:27 1. Veridise supports Eagen's scheme 17:53:29 2. Cypher Stack supports Eagen's scheme in a way that Veridise doesn't agree with (SLVer Bullet) 17:53:38 the end result is indeed that both firms support Eagen's scheme 17:53:42 Sorry, but to take this back a second: Rucknium, of course, you are allowed to believe a third review is justified. I just want to be clear, both Veridise and Cypher Stack currently agree on a proof to implement. They have independent arguments for why the proof is secure, and disagree with each other's arguments. 17:53:48 with the caveat that there is disagreement on how the support comes about from Veridise's side 17:53:53 We only released v3 the other day, so I would like clarification on if the Veridise comments pertain to this new version or not 17:53:57 I agree with jberman . The "third review" can occur in parallel to the implementation work, and any other code audit work. 17:54:06 If a third review were to occur 17:54:07 If you could confirm your understanding is they disagree on the road, not the destination, that would be great Rucknium. 17:54:47 Zk Security was prior brought up as a 3rd party to bring in for this review. I think it makes sense to bring them in prioritizing other work at this time, but to keep them in mind for a future 3rd review 17:54:56 and/or, the existing can be implemented, and then a third review can review both the math and the implementation 17:55:30 This wouldn't qualify as passing peer review in a journal since the reviewer(s) would have to agree that the author had a valid, specific, proof. 17:55:37 i don't think charging the same people for reviwing both the math and implementation is a good idea 17:55:40 I have never seen "Ok, here are two possibly-valid proofs" 17:55:44 i don't think charging the same people for reviewing both the math and implementation is a good idea 17:55:57 Choose which one you like 17:55:59 at least not at the same time 17:56:11 Unfortunately, happens all the time in pure math.... 😅 17:56:18 I think they do agree on the destination. 17:56:27 Are we allowing the axiom of choice? 17:56:33 Heresy! 17:56:42 Yes, but not the well ordering principle 17:56:51 Axiom of choice is always necessary for any real work. 17:56:57 Insider jokes? 17:57:07 I personally don't believe in free will and have (as inscribed in the universe itself) decided not to be convinced by any proof requiring even the idea of choice 17:57:39 rbrunner: The axiom of choice is an axiom one can use when writing proofs, with extensive debate over if it should be used and the impacts of it. 17:57:42