--- Day changed Wed Jan 06 2016
01:31 -!- jtimon [~quassel@103.red-80-26-235.adsl.dynamic.ccgg.telefonica.net] has joined #secp256k1
03:27 -!- jtimon [~quassel@103.red-80-26-235.adsl.dynamic.ccgg.telefonica.net] has quit [Ping timeout: 260 seconds]
07:05 < jonasschnelli> sipa: what's the drawbacks when using --with-bignum=no?
07:09 < sipa> jonasschnelli: slower :)
07:09 < sipa> GMP has a very fast modular inverse algorithm
07:09 < jonasschnelli> okay... thanks. Seems there is no bignum on apples 10.10 LLVM env.
07:09 < sipa> it needs gmp
07:09 < jonasschnelli> *no gmp
07:09 < jonasschnelli> thanks.
07:09 < sipa> eh you'll need to compile it and install it
07:10 < jonasschnelli> Yes... but not sure what dependencies i have to fight with... working on a tiny bitcoin dev tool for the app store.
07:10 < sipa> andytoshi has a nearly-finished native modular inverse, which is faster than what we have now, but still far away from being as fast as gmp's
07:10 < sipa> it's only a few% slowdown
07:11 < jonasschnelli> okay... performance is not an issue for the thing i'd like to achieve.
08:18 -!- jtimon [~quassel@103.red-80-26-235.adsl.dynamic.ccgg.telefonica.net] has joined #secp256k1
09:20 < maaku> Gmp has no dependencies
09:56 -!- jtimon [~quassel@103.red-80-26-235.adsl.dynamic.ccgg.telefonica.net] has quit [Ping timeout: 250 seconds]
09:59 -!- GAit [~GAit@2-230-161-158.ip202.fastwebnet.it] has joined #secp256k1
10:36 -!- GAit [~GAit@2-230-161-158.ip202.fastwebnet.it] has quit [Read error: Connection reset by peer]
10:37 -!- GAit [~GAit@2-230-161-158.ip202.fastwebnet.it] has joined #secp256k1
11:56 < gmaxwell> Anyone try SAW yet? http://saw.galois.com/tutorial.html
11:57 < sipa> i'm watching a presentation about it as we speak!
11:59 < gmaxwell> Tutorial has code equivilence checking examples.
11:59 < gmaxwell> Dettman spent time with the speaker the other day while I was spending time with people working on VST.
12:02 < andytoshi> gmaxwell: can we translate the asm stuff into llvm ir in any way?
12:02 < andytoshi> that's what this tool uses as its underlying code representation
12:04 < gmaxwell> andytoshi: maybe, but not in a way that might not undo bugs.
12:04 < andytoshi> mm yeah
12:04 < gmaxwell> LLVM IR is higher level than ASM.
12:04 < andytoshi> i wonder if we can use this to rediscover the old gej_add_ge bug .. by comparing it to the _var version
12:06 < gmaxwell> no, because they don't compute the same function unless you consider the affine output, and I can pretty much promise the SMT solver will not be able to reason about the field operations usefully. :)
12:06 < andytoshi> awww
12:06 < andytoshi> maybe it can check against a symbol version of the curve addition formulae tho
12:06 < andytoshi> and we can maybe teach it the equivalence of jacobian points with different z values
12:08 < gmaxwell> the issue with this kind of thing is that while we could teach an SMT solver what it needed to know, the input is so low level so its hard for the solver to reconstruct the field operations from it.
12:08 < gmaxwell> (this kind of thing is why I was paying more attention to VST, which actually could handle this... but the usability is poor.)
12:10 < gmaxwell> (VST could do it because it's input is compcert conversion of C to a COQ formalization and then we could just prove the field operations correct, then tell the prover given that correctness to convert the field operations in C to real the COQ ringtype... then COQ could verify proofs of the algebraic equivilence alongside the hoare stuff)
12:55 -!- jtimon [~quassel@103.red-80-26-235.adsl.dynamic.ccgg.telefonica.net] has joined #secp256k1
14:02 -!- GAit1 [~GAit@2.230.161.158] has joined #secp256k1
14:04 -!- GAit [~GAit@2-230-161-158.ip202.fastwebnet.it] has quit [Ping timeout: 240 seconds]
14:33 -!- jtimon [~quassel@103.red-80-26-235.adsl.dynamic.ccgg.telefonica.net] has quit [Ping timeout: 245 seconds]