4 ms·

Oh, the performance is the worst. Just initializing the database with 6 images ran my 16GB desktop out of memory. I was able to get it running on a 128GB server

Oh, the performance is the worst. Just initializing the database with 6 images ran my 16GB desktop out of memory. I was able to get it running on a 128GB server I have. The root of it seems to be that something somewhere is using Peano naturals rather than binary ones, and the image timestamps are in the billions. So I worked around it by setting all the timestamps to 1: timestamp <- modificationTimeHiRes <$> getFileStatus filepath return $ DB.MkImage DB.N0 filepath (int_to_n 1) If I banned Peano naturals from all Set-level code and used a better extraction library, I don't see why it couldn't be as fast as Haskell. It might also be worth setting the Strict flag on Haskell for the generated code, since Coq seems designed to target ML, which is strict. Anyone have an idea for an Idris article? Maybe "How to make a Bitcoin exchange or Ethereum contract that's 100% guaranteed not to rob you of your money?"

iso-8859-1 9y ago
It's a great idea! Bitcoin needs more formal verification. I wonder how much of e.g. Lightning Network can be proven, assuming SHA256 collisions can't be found, miners include transactions and signatures are unfalsifiable and not malleable. Roasbeef wanted to do it in TLA+, but I am not sure he will find the time.
sddfd 9y ago
Why not use a binary number representation? They are in the library: https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNat.htm https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNa... If you use Z, even the Omega tactic (solver for presburger arithmetic) should work.
- MichaelBurge 9y ago
  (* edit: profquail below points out that the Integer variant of the Z extraction module has a less strongly-worded disclaimer. Just importing it would probably fix the described memory issue. *) https://github.com/coq/coq/blob/307f08d2ad2aca5d48441394342af4615810d0c7/plugins/extraction/ExtrHaskellZInteger.v https://github.com/coq/coq/blob/307f08d2ad2aca5d48441394342a...
  - profquail 9y ago
    Can it extract [Z] to some bigint implementation based on gmp? That should still be safe but provide better performance than using Peano arithmetic.
oh_sigh 9y ago
Is there a reason coq can't fake peano naturals with a much more performant substitute?
- sddfd 9y ago
  It can. He didn't bother to do it.
  - Karrot_Kream 9y ago
    Can you direct me to docs that show how to do this?
pron 9y ago
> Maybe "How to make a Bitcoin exchange or Ethereum contract that's 100% guaranteed not to rob you of your money?" I think you'll find that specifying that and proving it is orders of magnitude more complicated and costly than the example in this post. I think that at this point, the most optimistic estimates are that producing software like that (meaning, verifying global correctness properties) would require about 1 day per line of code (and we're not there yet, but 2-5x that), and that is provided that the overall program is no more than a few thousand lines and uses just the simplest algorithms possible. There are other formal methods that allow cheaper verification for the cost of weaker evidence of correctness, like test generation from specifications, model checking of small, finite instances etc.. It is an open question how much confidence formal proofs actually add. For example, while model checking has found errors in informal (although peer-reviewed) proofs several times, I am not aware of cases where a program verified with a model checker on small instances turned out to be incorrect.

iso-8859-1 9y ago

It's a great idea! Bitcoin needs more formal verification. I wonder how much of e.g. Lightning Network can be proven, assuming SHA256 collisions can't be found, miners include transactions and signatures are unfalsifiable and not malleable. Roasbeef wanted to do it in TLA+, but I am not sure he will find the time.

sddfd 9y ago

Why not use a binary number representation? They are in the library: https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNat.htm https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNa... If you use Z, even the Omega tactic (solver for presburger arithmetic) should work.

MichaelBurge 9y ago
(* edit: profquail below points out that the Integer variant of the Z extraction module has a less strongly-worded disclaimer. Just importing it would probably fix the described memory issue. *) https://github.com/coq/coq/blob/307f08d2ad2aca5d48441394342af4615810d0c7/plugins/extraction/ExtrHaskellZInteger.v https://github.com/coq/coq/blob/307f08d2ad2aca5d48441394342a...
- profquail 9y ago
  Can it extract [Z] to some bigint implementation based on gmp? That should still be safe but provide better performance than using Peano arithmetic.

oh_sigh 9y ago

Is there a reason coq can't fake peano naturals with a much more performant substitute?

sddfd 9y ago
It can. He didn't bother to do it.
- Karrot_Kream 9y ago
  Can you direct me to docs that show how to do this?

pron 9y ago

> Maybe "How to make a Bitcoin exchange or Ethereum contract that's 100% guaranteed not to rob you of your money?" I think you'll find that specifying that and proving it is orders of magnitude more complicated and costly than the example in this post. I think that at this point, the most optimistic estimates are that producing software like that (meaning, verifying global correctness properties) would require about 1 day per line of code (and we're not there yet, but 2-5x that), and that is provided that the overall program is no more than a few thousand lines and uses just the simplest algorithms possible. There are other formal methods that allow cheaper verification for the cost of weaker evidence of correctness, like test generation from specifications, model checking of small, finite instances etc.. It is an open question how much confidence formal proofs actually add. For example, while model checking has found errors in informal (although peer-reviewed) proofs several times, I am not aware of cases where a program verified with a model checker on small instances turned out to be incorrect.