--- Log opened Mon Jul 31 00:00:15 2023
01:05 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
04:38 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has quit [Quit: My iMac has gone to sleep. ZZZzzz…]
04:51 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
06:01 -!- siv2r [~siv2rmatr@2001:470:69fc:105::fed3] has quit [Remote host closed the connection]
06:02 -!- stratospher[m] [~stratosph@2001:470:69fc:105::2:728e] has quit [Read error: Connection reset by peer]
06:02 -!- BlueMatt[m] [~bluemattm@2001:470:69fc:105::1:5092] has quit [Write error: Connection reset by peer]
06:02 -!- sipa [~sipa@user/sipa] has quit [Remote host closed the connection]
06:15 -!- sipa [~sipa@user/sipa] has joined #secp256k1
06:17 -!- jonatack3 [~jonatack@user/jonatack] has quit [Read error: Connection reset by peer]
06:17 -!- jonatack3 [~jonatack@user/jonatack] has joined #secp256k1
06:25 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
06:25 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
06:36 -!- preimage [~halosghos@user/halosghost] has joined #secp256k1
06:59 < roconnor> What time is the meeting?
07:00 -!- BlueMatt[m] [~bluemattm@2001:470:69fc:105::1:5092] has joined #secp256k1
07:00 -!- siv2r [~siv2rmatr@2001:470:69fc:105::fed3] has joined #secp256k1
07:00 -!- stratospher[m] [~stratosph@2001:470:69fc:105::2:728e] has joined #secp256k1
07:01 < fanquake> in 1 hour
07:04 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
07:04 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
08:01 < real_or_random> meeting :)
08:01 < sipa> hi
08:01 < hebasto> hi
08:01 < real_or_random> sipa nickler roconnor 
08:01 < roconnor> hi
08:01 < nickler> hi
08:02 < real_or_random> topics?
08:02 < hebasto> response to new Cirrus CI limits?
08:02 < sipa> Nothing from me.
08:03 < real_or_random> formal verification efforts 
08:03 < nickler> nothing from me either
08:03 < real_or_random> yeah, responde to cirrus ci limits
08:04 < hebasto> https://cirrus-ci.org/blog/2023/07/17/limiting-free-usage-of-cirrus-ci/
08:04 < real_or_random> I think we should follow bitcoin core... and the solution there isn't clear yet.
08:04 < sipa> Can we self-host workers?
08:04 < real_or_random> AFAIU, one suggestion is to move linux tasks to self-hosted workers and move windows/macos tasks to github actions
08:05 < sipa> We can't self host the windows/macos ones?
08:05 < hebasto> it might be possible but not tested yet
08:06 < real_or_random> hebasto: do you know who hosts the existing linux workers?
08:06 < sipa> It's certainly harder, and we might not want to do that.
08:06 < sipa> But I'm not very happy about increasing reliance on github.
08:06 < hebasto> Marco does
08:07 < real_or_random> sipa: yep, though you can argue the other way around: we trust github anyway...
08:07 < hebasto> if we are interested to host win/macos workers, I can test them
08:08 < real_or_random> I believe we should try hosting win/macos only if core does the same
08:08 < sipa> @real_or_random Oh my problem isn't with trusting them. It's about being able to move off them.
08:08 < sipa> Even if we choose not to do that, I don't like being in a situation where we can't.
08:09 < hebasto> for now, in core there are no people who both interested in hosting and has such opportunities
08:10 < real_or_random> and we should probably ask marco if it's okay that we move our linux  tasks to these hosts as well. alternatively, we could try to ask blockstream to add hosts... in secp256k1-zkp, we'll end up with the same issue in the end if we want to keep a ci. so if we end up hosting these anyway, we could donate to core/secp
08:11 < real_or_random> sipa: i see. but I don't think github is any different from cirrus here. if we need to leave github, cirrus ci also won't work anymore (because they support only github currently)
08:12 < real_or_random> in that sense cirrus is strictly worse: we need to move away from cirrus if we don't want to use *either* of github or cirrus.
08:12 < sipa> Hmm, ok.
08:12 < hebasto> also cirrus seems being run by a very small team, probably the only guy
08:13 < real_or_random> yep, I count two guys, but yes, it's a small team
08:14 < fanquake> I don't think it's that no-one in core is bothered, it's actually unclear if self-hosted would even work?
08:14 < fanquake> I'm pretty sure if someone opened a PR to support self hosted for macos and win, it'd be considered, like any other PR, but nobody has actually done that
08:15 < real_or_random> I agree. it's just a lot of (annoying) work to host these and try
08:16 < real_or_random> has this been discussed at the core meeting? I think it should, it's a somewhat big issue with an upcoming deadline.
08:16 < fanquake> I think it's somewhat unlikely that marco would (or should even be required) to front the costs to host even more CI infra, and I'm not sure we should add even more cross-project burden to another individual
08:16 < fanquake> It's kinda nuts that apparently we can't find any org in the space (excluding those who already contribute to it) to spend a few hundred $$ on CI costs etc
08:17 < sipa> If money is an issue I'm sure we can find some?
08:17 < real_or_random> I think the problem is that it's not just money
08:17 < sipa> Indeed.
08:17 < real_or_random> or... it's complicated. the "just money" part is available but cirrus' price structure is very strange
08:18 < sipa> Ok
08:18 < real_or_random> if we just buy cirrus credits for core+secp, we'll up burning a 5-digit dollar amount / month
08:18 < fanquake> Yea, money is one portion, and I know we've been reaching out to people to try and raise some more already
08:19 < sipa> @real_or_random Ok that's ridiculous.
08:19 < hebasto> I don't think sponsor's money should be used to pay citrus. Rather to pay to win/mac cloud service.
08:19 < real_or_random> which is a bit unreasonable. that money would pay us more than an engineer 
08:19 < sipa> Right.
08:20 < real_or_random> so that means if we want to stay on cirrus, we'll need money + work.
08:21 < real_or_random> alternatively, we could move *everything* to gh actions. it's free with an unlimited plan for open source. at least currently 
08:21 < sipa> It sounds like perhaps this is primarily something to discuss on the Bitcoin Core meeting, and we can probably follow whatever is done there?
08:21 < real_or_random> sipa: yep, I think that's best
08:22 < fanquake> so someone in this project will start setting up self hosted runners / maintaining them etc?
08:22 < fanquake> as mentioned, we already do this, and are likely to be adding more, but I don't think we'd want to combine the two, and give Marco even more work/costs
08:23 < fanquake> fwiw I think most of the infra is now on hetzner
08:23 < real_or_random> i don't know. if core decides to add self-hosted runners paid by Marco, we can still reconsider
08:24 < fanquake> Ok. Just to be clear, Core already has self-hosted runners, paid for by Marco
08:24 < real_or_random> yes, I know
08:24 < fanquake> Our current cirrus costs have been covered mostly by another org
08:25 < sipa> Well Marco shouldn't be paying for those; I can't imagine it's an amount we couldn't find sponsorship for.
08:25 < sipa> I think the bigger question is about maintenance work.
08:25 < real_or_random> if you ask me, I don't want Marco to pay for any of these. For current hosts, for additional core hosts, and for potential secp hosts  
08:25 < sipa> Indeed.
08:26 < fanquake> I agree, and we've been trying to get more orgs to pay these costs
08:26 < real_or_random> without success apparently?
08:26 < sipa> I had no idea this was even an issue.
08:26 < sipa> Chaincode has hardware too, maybe some things can run there?
08:27 < fanquake> Yea, they are one of the orgs already sponsoring some costs, unsure about their hardware
08:27 < fanquake> Brink is likely to start contributing as well 
08:27 < fanquake> I assume we wouldn't have any trouble also getting blockstream to contribute
08:27 < real_or_random> but yeah, I think this belongs to the core meeting.
08:28 < real_or_random> (ok yeah, please don't assume anything for now, we haven't talked to anyone, but I believe it's reasonable to ask) 
08:30 < real_or_random> at least it doesn't make sense to decide/do anything now, before this has been been discussed with core  
08:31 < sipa> agree
08:31 < hebasto> sure
08:32 < real_or_random> so next topic?
08:32 < real_or_random> verification efforts... and https://github.com/bitcoin-core/secp256k1/pull/1319#issuecomment-1656593371 in particular
08:33 < real_or_random> for fiat-c, our rough plan was to replace the C code first, and then think about asm (cryptopt)
08:34 < real_or_random> replacing C turned out a bit harder than expected. 
08:34 < real_or_random> fiat had to make some changes to be compatible with our abstract uint128 implementation
08:35 < real_or_random> we have these changes now, and the resulting C code is in #1319, but even that one is not fully compatible to our int128 interface 
08:36 < real_or_random> because the fiat C code uses pass-by-value/return-by-value for structs, whereas we use pointers everywhere
08:36 < sipa> ugh
08:37 < real_or_random> this can be fixed by wrappers (as in the PR) and the resulting code works, and is basically on par with our C code (well clang generates different code, a few 0.1% slower) 
08:38 < sipa> ok
08:38 < real_or_random> now the question is how to move forward... and this raises questions we perhaps should have dealt with earlier
08:39 < real_or_random>  - the code in the PR is not beautiful, but it increases assurance. how would we want to maintain this? we can't meaningfully touch it unless we touch fiat-crypto
08:40 < real_or_random>  - roconnor's plan is to verify the field operations independently. this would retain our "nice" code, but if we want to rely on this, the same question about maintainability appears. then with VST instead of fiat-crypto 
08:40 < sipa> That's a good question.
08:41 < roconnor> I should also point out another wrinkle is that VST doesn't support  pass-by-value/return-by-value for structs, so the new code cannot be reasoned about in VST.
08:42 < real_or_random> arguably, the fiat part is a bit more limited in scope. it's probably okay to not touch fe_mul_inner and fe_sqr_inner for some point?
08:43 < roconnor> libsecp is currently in an interesting state where it seems to entirely fall into VST's domain of C code it can reason about, and doesn't even depened on any standard library whose functions would need their own formal specifications that would be unchecked.
08:43 < roconnor> So currently essentially the entire codbase can totally be reasoned about within VST.
08:46 < roconnor> I could refocus my verification efforts on the field code and the resulting proof would be of slightly higher assurance than the fiat-crypto, but maybe less maintainable.  We can debate the the various aspects of what maintable means in the two contexts.
08:46 < real_or_random> the idea to have the entire libary verified sounds great, but then we'll all need to learn VST ^^ and development will be slow. that's a huge commitment
08:47 < roconnor> It isn't so bad for the verifaction effort to be behind the production code.  int128 has change a bit over the year, and I just post-facto verify it.
08:48 < real_or_random> yep, true
08:48 < real_or_random> I mean it would certainly be interesting to compare the VST efforts for the field code to fiat
08:48 < roconnor> The biggest problem with VST might be that a fragement of the work depends on a prioriatery program.
08:49 < real_or_random> not sure if it helps us here, but it won't hurt (and that's okay if you simply redirect your attention?) 
08:50 < roconnor> Sure, if you think it helps, I'm happy to work on it.  The field code is straight line with no branches, so is in some sense pretty easy to reason about.
08:50 < roconnor> is it just the inner functions?
08:51 < real_or_random> fiat covers only mul_inner and sqr_inner
08:51 < roconnor> so even easier.
08:51 < real_or_random> but I can't speak for anyone else... sipa nickler: any opinions here? 
08:51 < roconnor> I'm not sure what the conclusion will be but since I plan to do it anyways I can start work on it.
08:53 < sipa> Sorry, not feeling very well today, I have a hard time focusing.
08:54 < real_or_random> another question is whether we want to give up on the idea that we first need the fiat C code before we can introduce cryptopt
08:54 < sipa> I'm going to be on vacation 2nd-13th, so I probably won't have much to say next meeting as well.
08:54 < real_or_random> I don't think so... as long as we're confident in fiat+cryptopt, we could replace the asm 
08:54 < real_or_random> ok
08:55 < sipa> If we had independent verification of asm code (e.g. cryptoline), maybe the situation would be different.
08:56 < real_or_random> you mean for cryptopt?
08:56 < sipa> Yeah.
08:57 < real_or_random> well cryptopt is fed through fiat-crypto again, so its output is "verified"
08:57 < real_or_random> but it may help to understand what is actually guaranteed and what not
08:57 < real_or_random> (e.g., there was the clobber issue) 
08:58 < real_or_random> anyway, it think it makes more sense to discuss on github then
08:58 < sipa> right, and cryptopt has a verification step too, which is independent from fiat, right?
08:59 < sipa> right
08:59 < real_or_random> I don't think so. at least the README says that it depends on fiat for verification. and it doesn't mention another step
09:00 < real_or_random> ok then end of meeting... we're at the top of the hour anyway
09:06 < roconnor> ugh, in the inner functions r and a might alias.  This specification is going to be a little annoying.
09:40 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has quit [Quit: My iMac has gone to sleep. ZZZzzz…]
10:14 < real_or_random> yep, AFAIU, this is another thing which is currently not formalized in fiat
10:15 < real_or_random> ok at least the "assembly checker" does not support this https://github.com/mit-plv/fiat-crypto/issues/1615
10:25 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
11:05 -!- DeanGuss [~dean@user/deanguss] has quit [Remote host closed the connection]
11:06 -!- DeanGuss [~dean@nonplayercharacter.me] has joined #secp256k1
11:06 -!- DeanGuss [~dean@nonplayercharacter.me] has quit [Changing host]
11:06 -!- DeanGuss [~dean@user/deanguss] has joined #secp256k1
12:17 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has quit [Quit: My iMac has gone to sleep. ZZZzzz…]
12:56 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
13:05 -!- jb55 [~jb55@user/jb55] has quit [Quit: jb55]
13:58 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has quit [Quit: My iMac has gone to sleep. ZZZzzz…]
14:13 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
14:13 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
14:51 -!- preimage [~halosghos@user/halosghost] has quit [Quit: WeeChat 4.0.2]
14:51 < roconnor> I'll probably finish off the correctness of secp256k1_modinv64_divsteps_62_var first before moving to the field ops.
14:56 < roconnor> sipa: Just finished this lemma
14:56 < roconnor> Lemma transSs n st : DivStep.delta st <= 0 -> Z.of_nat n <= 1 - DivStep.delta st ->
14:56 < roconnor>   transN n st = {| u := 2^(Z.of_nat n); v := 0;
14:56 < roconnor>     q := (-modInv (DivStep.f st) (2^(Z.of_nat n)) * DivStep.g st) mod (2^(Z.of_nat n)); r := 1 |}.
14:57 < roconnor> no requirement that g be odd.
15:01 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
15:01 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
15:36 -!- siv2r [~siv2rmatr@2001:470:69fc:105::fed3] has quit [Ping timeout: 246 seconds]
15:36 -!- stratospher[m] [~stratosph@2001:470:69fc:105::2:728e] has quit [Ping timeout: 246 seconds]
15:36 -!- sipa [~sipa@user/sipa] has quit [Ping timeout: 246 seconds]
15:36 -!- BlueMatt[m] [~bluemattm@2001:470:69fc:105::1:5092] has quit [Ping timeout: 246 seconds]
23:06 -!- tromp [~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl] has joined #secp256k1
23:41 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has quit [Remote host closed the connection]
23:41 -!- ghost43 [~ghost43@gateway/tor-sasl/ghost43] has joined #secp256k1
--- Log closed Tue Aug 01 00:00:15 2023