--- Log opened Mon Dec 04 00:00:48 2023
01:00 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
02:12 -!- sgiath [~sgiath@mail.sgiath.dev] has quit []
04:44 -!- kanzure [~kanzure@user/kanzure] has joined #secp256k1
04:55 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has quit [Quit: Textual IRC Client: www.textualapp.com]
04:58 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
05:36 -!- jon_atack [~jonatack@user/jonatack] has joined #secp256k1
05:37 -!- jonatack [~jonatack@user/jonatack] has quit [Ping timeout: 252 seconds]
07:00 < nickler> hi
07:01 < hebasto> hi
07:01 < real_or_random> hi, meeting :)
07:01 < roconnor> hi
07:01 < real_or_random> sipa
07:02 < real_or_random> (I'm on a train... one could that connectivity is good enough for an IRC meeting but you'll never know... ^^)
07:03 < nickler> Thanks real_or_random for the CONTRIB.md review. Will your comments shortly.
07:03 < real_or_random> :)
07:03 < real_or_random> one topic is roconnor's verification progress here https://github.com/bitcoin-core/secp256k1/pull/1319#issuecomment-1821834018
07:04 < real_or_random> and its implications to the fiat code
07:05 < real_or_random> so the tl;dr is that roconnor has verified  secp256k1_fe_mul_inner and secp256k1_fe_sqr_inner in VST, the exact same functions as covered by the fiat crypto efforts
07:07 < real_or_random> and AFAIU the assurance is better than what fiat currently offers. (I guess they're formally incomparable if you consider all caveats, but at least you took into account the use of restrict, which is currently not covered by fiat)
07:07 < real_or_random> is this right?
07:08 < sipa> hi
07:08 < roconnor> VST doesn't verify restrict per se, but I am able to express the condition that it implies with the VST specification.
07:08 < real_or_random> I see
07:08 < roconnor> And thus I'm able to pass the a != b assert with my precondition.
07:09 < roconnor> er verify
07:09 < real_or_random> in the PR you say "With this VST proof in hand we have comparable assurance to what the fiat-crypto code gives us, but in a way that can let us proof the (functional) correctness of subsequent functions."
07:10 < real_or_random> that seems true to me... also your proofs vs fiat have the same problems in terms of "continuous verification". these are currently one-shot efforts
07:11 < real_or_random> if we touch the code, we'll lose the guarantee, and we'll need to ask fiat people or you to take action to get a guarantee again. that's not great currently, but my point is that it's the same for both approaches
07:11 < roconnor> Yes, but in the case of fiat you wouldn't want to touch the generated code.  If you want to change it, you'd update it in fiat.
07:12 < real_or_random> right
07:12 < roconnor> It's particularly problematic in the case of VST where one step (converting C code to Coq C AST data structure) requires a proprietary program.
07:13 < nickler> roconnor: this is really great, thanks a lot. Do the proofs only cover 5x52, or also 10x26?
07:13 < roconnor> I only did 5x52.
07:13 < real_or_random> good point 
07:14 < nickler> Would be interesting to hear from the fiat people if they agree with the assessment.
07:14 < sipa> i kind of wish someone would spend the time to prove the compiled code correct in cryptoline... if that works (which it very well might not), we can probably run it continuously, even with changing code
07:15 < roconnor> I'm not familiar with cryptoline
07:16 < nickler> I wonder if we should link to the proofs in the code (or mark it otherwise) to remember that we invalidate the proofs when we change them. And mark other functions similarly that have been proven in VST
07:17 < real_or_random> nickler: I think that's a good idea
07:18 < nickler> roconnor: what's your confidence in the correctness of the spec?
07:19 < real_or_random> it doesn't change anything about the underlying problem that touching the code invalidates the analysis but it may influence our willingness to accept PRs.
07:19 < roconnor> My confidence is fairly high.  Confindence will increase as we prove correct the functions higher up in the call chain.
07:20 < nickler> good!
07:20 < sipa> roconnor: it takes x86 or ARM asm (actually a transcript of executed instructions, so unrolled) and proves statements about it... presumably it has some non-proven model of the CPU instructions, but in our case those instructions are likely very simple too
07:20 < real_or_random> roconnor: there's really no other than running this proprietary tool? I guess we can't get a license to run it in CI? ^^
07:21 < roconnor> real_or_random: Other than reimplementing a free version of the same tool.
07:21 < sipa> roconnor: is that doable by hand?
07:21 < roconnor> I'm not sure if the tool itself is formally verified.  Maybe I should ask.
07:22 < roconnor> But the tool converts C code to a Coq datastructure that represents code. But it does some other transformations as well.
07:22 < real_or_random> I mean we have access to private CI runners etc. we could install the tool there without making it available to others. I wonder what the license says 
07:23 < roconnor> It does some source-code to souce-code translations that make sure there is only one memory access per command, introducing temporaries and restructuring if statements in the process.
07:23 < real_or_random> sipa: do you agree with the idea to "mark" verified functions in the source/link to proofs? 
07:23 < sipa> real_or_random: yes
07:24 < real_or_random> I'll note that in the formal methods issue
07:24 < roconnor> nickler: also we only verify the int128_struct varient of this code (due to lack of int128 support).
07:25 < real_or_random> hm right that's another difference
07:25 < roconnor> Another thing we could do, which I don't actually recomment, is to take the Coq AST and generate C code from it.
07:25 < nickler> If we don't expect to make changes that don't invalidate the proofs, we could also move the proven functions into separate files, hash them and check against fixed hash in CI. But that would also invalidate renames, comments, etc. Meh.
07:26 < nickler> roconnor: but we proved that int128_struct behaves as int128 (should)
07:26 < sipa> how about adding a comment that say "this code: [copy of the exact code that was proven] was proven under [these conditions/compilation flags/config options/...] with tool [x] [link to proof]"
07:26 < roconnor> more or less.  we moved they meet certain specifications that we expect are true for int128.
07:27 < real_or_random> roconnor: well that sounds good enough
07:27 < roconnor> *we proved
07:27 < real_or_random> so fiat's scope includes 10x26 and normal ints (but issues with our int128 abstraction) but no restrict semantics. and the scope of your VST proof has restrict but limited support for normal ints
07:28 < roconnor> did fiat generate 10x26?  It wasn't part of #1319.
07:28 < real_or_random> hm I may misremember
07:28 < real_or_random> sipa: you want to restate the entire code in the comment?
07:29 < sipa> real_or_random: yes; because i think if we change the code, but don't (yet) go through the effort of updating the proofs, having the proof for the previous version may still be useful if a human reviewer can have some confidence in their equivalence
07:29 < roconnor> I don't quite know what you mean by limited support for normal ints, but I don't think VST has such limitations.
07:29 < sipa> real_or_random: if it's too much to include a full copy in the comments directly, it could be a separate file or so
07:29 < nickler> sipa: we could also do a copy-on-write, i.e. only copy the code when we change it
07:30 < sipa> nickler: yes, *if* we remember to that, that's equivalent
07:30 < sipa> it's a bit harder if the function has many dependencies that could change from under it, though
07:30 < nickler> just add the reminder to the comment xD
07:30 < sipa> which i guess isn't the case for secp256k1_fe_mul_inner, but it may be the case for stuff higher up the stack
07:30 < real_or_random> (I think fiat has support for code that has at most uint64_t / 10x26: https://gist.github.com/andres-erbsen/a8f6c694e80168354b19710fc811c5c4)
07:30 < roconnor> I mean the link to the proof will be a git commit that also include the code that (should have) been used to generate the proof.
07:31 < real_or_random> but yes, you're right, it makes sense for a human reviewer. could copy-on-write it into an #if 0 block or something ^^ anyway, details 
07:32 < real_or_random> the big question is what we do with the fiat PR then
07:32 < nickler> roconnor: I don't see the code in the link you provided (https://htmlpreview.github.io/?https://github.com/ElementsProject/simplicity/blob/verif_field_5x52_int128_impl_0/alectryon/verif_field_5x52_int128_impl.v.html). I guess it's somewhere else?
07:33 < roconnor> Indeed.  The code is in https://github.com/BlockstreamResearch/simplicity/blob/verif_field_5x52_int128_impl_0/C/secp256k1/field_5x52_int128_impl.h
07:34 < real_or_random> I think some stuff should be addressed before we consider this: a) int128 abstraction , b) support for restrict 
07:34 < nickler> real_or_random: would be nice to hear from the fiat crypto guys again before closing, maybe we can just ask them if they have final words before closing or something?
07:34 < roconnor> I can probably make the connection more clear somehow.
07:34 < real_or_random> but even if these additions are there, I don't want to promise that there's a high chance of inclusion
07:34 < real_or_random> nickler: yeah, for sure
07:35 < real_or_random> we could at least ask them for their opinion, say that we'd love to have these aforementioned features, but that it will still be unsure if we'll want to include it then
07:36 < roconnor> real_or_random: if they solved those two problems, I would prove their generated code correct.
07:36 < roconnor> and then I would recommend using it.
07:36 < real_or_random> you mean you would prove the fiat-c output in VST? 
07:36 < roconnor> yes.
07:37 < real_or_random> that sounds like twice the effort but yeah, happy to take this xD
07:37 < roconnor> in fact they don't have to even handle restrict.  We can just hack their output to add it to the signature, and it will be included in the VST specification.
07:38 < real_or_random> makes sense
07:38 < roconnor> Not quite twice the effort since the specification creating work doesn't need to be repeated.  That was like half or a third of the effort.
07:38 < real_or_random> would you include 10x26 then?
07:38 < roconnor> I'm assuming the underlying algorithm is identical.
07:39 < real_or_random> yep
07:39 < real_or_random> yet another question is cryptopt. we could use cryptopt asm without having fiat's C code. not sure how this would compare to the best current compiler output . I mean it's a hyper optimizer, it could certainly be faster than what a compiler will produce even though it has some formal guarantees
07:39 < roconnor> In principle I would.  However, I mostly did this field work in order to stop you folks from accepting a PR that includes structures that are passed by value.
07:39 < roconnor> If they end up passing structs by reference then I would probably just do the proofs whenever.
07:40 < real_or_random> I see
07:40 < roconnor> I would have done this field work evetually anyways, I just moved around the timeline.
07:42 < real_or_random> but I think, I don't fully understand. if they implement support for restrict and our int128, they'd still pass by value, I guess?
07:42 < real_or_random> so how would this help you? do we need to ask them also for pass by pointer?
07:42 < roconnor> pr 1319 uses our int128 for some definition of our int128.
07:44 < real_or_random> right though it doesn't look optimal yet 
07:45 < real_or_random> other points? i'm volunteering to post a summary of this discussion to the PR
07:45 < roconnor> My thoughts are written at https://github.com/bitcoin-core/secp256k1/pull/1319#issuecomment-1821834018
07:46 < real_or_random> (Perhaps ChatGPT will volunteer to write a first draft of the summary. :P) 
07:48 < roconnor> We could copy the VST formal specification as a comment to the functions that are proved correct.
07:48 < roconnor> in addition to the topic about linking to the proof.
07:48 < real_or_random> indeed
07:50 < roconnor> I guess the specifications make reference to other Coq functions, including special purpose ones written specifically for the specification, but even still.
07:52 < real_or_random> more to add to this discussion?
07:52 < real_or_random> other last-minute topics?
07:53 < sipa> none from me
07:53 < nickler> release is scheduled on a friday :)
07:54 < real_or_random> for the release, I still want to work on https://github.com/bitcoin-core/secp256k1/issues/1095 this week. Perhaps that will be too late to get ACKs until the release, but I feel that shouldn't stop me ^^
07:54 < real_or_random> oh I'll be out of office on that friday...
07:56 < real_or_random> would it make sense to reschedule to 13th or 14th?
07:56 < nickler> I guess we can move it a few days back and coordinate the exact time among the maintainers
07:56 < real_or_random> back is what direction?
07:56 < nickler> real_or_random: both would work for me
07:56 < nickler> real_or_random: later
07:57 < real_or_random> 13, 14, 19, 21, 22 would all work for me 
07:57 < sipa> all ok for me
07:59 < real_or_random> nickler: any pref?
08:00 < real_or_random> 21 sounds good to me
08:01 < nickler> no preference
08:01 < real_or_random> ok, then 21
08:02 < sipa> ok
08:02 < nickler> ok
08:03 < real_or_random> end of meeting?
08:04 < real_or_random> I've updated the milestone
08:06 < sipa> ack
08:40 -!- preimage [~halosghos@user/halosghost] has joined #secp256k1
09:44 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has quit [Quit: My iMac has gone to sleep. ZZZzzz…]
10:27 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
11:17 -!- jamesob [~jamesob@108.44.248.162] has quit [Ping timeout: 260 seconds]
11:22 -!- ajonas__ [sid385278@id-385278.helmsley.irccloud.com] has joined #secp256k1
11:22 -!- stratospher__ [uid514069@id-514069.ilkley.irccloud.com] has joined #secp256k1
11:22 -!- FelixWeis__ [sid154231@id-154231.hampstead.irccloud.com] has joined #secp256k1
11:25 -!- ajonas [sid385278@id-385278.helmsley.irccloud.com] has quit [Ping timeout: 252 seconds]
11:25 -!- stratospher [uid514069@id-514069.ilkley.irccloud.com] has quit [Ping timeout: 252 seconds]
11:25 -!- FelixWeis_ [sid154231@id-154231.hampstead.irccloud.com] has quit [Ping timeout: 252 seconds]
11:25 -!- preimage [~halosghos@user/halosghost] has quit [Ping timeout: 252 seconds]
11:25 -!- stratospher__ is now known as stratospher
11:25 -!- ajonas__ is now known as ajonas
11:26 -!- preimage [~halosghos@user/halosghost] has joined #secp256k1
11:42 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has quit [Quit: My iMac has gone to sleep. ZZZzzz…]
11:51 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
12:58 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has quit [Quit: My iMac has gone to sleep. ZZZzzz…]
13:02 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
13:17 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has quit [Quit: My iMac has gone to sleep. ZZZzzz…]
13:23 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
14:06 -!- preimage [~halosghos@user/halosghost] has quit [Quit: WeeChat 4.1.1]
14:41 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has quit [Quit: My iMac has gone to sleep. ZZZzzz…]
14:42 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
14:55 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has quit [Quit: My iMac has gone to sleep. ZZZzzz…]
14:56 -!- lbia [~lbia@user/lbia] has quit [Ping timeout: 246 seconds]
15:19 -!- lbia [~lbia@user/lbia] has joined #secp256k1
16:47 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
16:48 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has quit [Client Quit]
16:51 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
16:52 -!- ghost43_ [~ghost43@gateway/tor-sasl/ghost43] has quit [Ping timeout: 240 seconds]
18:38 -!- bob_x1 [~bob_x@user/bob-x1/x-8934932] has quit [Remote host closed the connection]
18:38 -!- bob_x1 [~bob_x@user/bob-x1/x-8934932] has joined #secp256k1
23:09 -!- bob_x1 [~bob_x@user/bob-x1/x-8934932] has quit [Remote host closed the connection]
23:10 -!- bob_x1 [~bob_x@user/bob-x1/x-8934932] has joined #secp256k1
23:13 -!- bob_x1 [~bob_x@user/bob-x1/x-8934932] has quit [Remote host closed the connection]
23:13 -!- bob_x1 [~bob_x@user/bob-x1/x-8934932] has joined #secp256k1
23:37 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
--- Log closed Tue Dec 05 00:00:49 2023