bkase

I work on the tooling layer for zkapps on Mina — Great questions!

I think in the future the overhead will improve significantly, and we can already see incremental improvements in some proof systems. For Kimchi (the proof system we’ve built for zkapps/Mina), we've instead focused on features — like infinite recursion. To really see the performance overhead reduce, we’ll need to push more of the compute into silicon (think opcodes designed for zk similar to the ones we have now to accelerate RSA). In the meantime, modern processors are fast enough that this overhead doesn’t hold back many sorts of applications.

On fixed inputs: Kimchi is “universal” in that it can recursively compose arbitrary circuits efficiently — including ones with different public and private inputs and including ones that haven’t been defined yet. This is what powers zkapps and zkapps’ ability to recursively compose circuits on itself (think application-specific rollups).

Randomness: Modern blockchains have mechanisms for trustlessly agreeing on securely generated random seeds. We can tap into that and use mechanisms like verifiable random functions (which Mina uses internally during consensus) to securely manage randomness (caveat: we haven’t built out the randomness APIs for zkapps yet so there may be some nuance here that we haven’t run into yet). If you want to learn more about how this works in Mina, read up on Ouroboros Samasika, Mina Protocol’s consensus mechanism.

Prevent replay attacks: Blockchains are designed for this :). Basically increment a nonce and feed the current nonce as one of the public inputs to the zkapp.

Remote attestation: This requires nuance to define properly as there are different solutions to different versions of this problem. I’ll outline a few here:

1. Consider the case where you trust the entity that attesting to something and they can upgrade their backend: the entity adds a snark friendly signature to their endpoint and you check the signature within the zkapp (remember since they run locally, you execution can just make async network requests)

2. Consider the case where you trust the entity but can’t convince them to change their API: here you can verify the contents of the response against the TLS signature that already exists in the modern web. Caveat: this is still a work in progress, we’re currently calling it zkOracles

3. Consider the case where you don’t trust the entity — in this case we’re talking about reading information from other zkapps or blockchains. Luckily, these all come with signatures in different shapes and sizes so the problem becomes efficiently verifying those signatures from within the zkapp. You can solve this in modern plonkish zk proof systems with custom gates. Caveat: this is also a work in progress for zkapps in Mina.

Unfortunately, I don't actually have access to NVidia hardware anymore -- but I would be happy to accept a PR from someone who can get this to run!

Which links specifically are broken?

Hmm I'll take a look at that. Yes code is here: https://github.com/bkase/CUDA-grep

One of the authors here: Happy to answer any questions. Keep in mind this was a school project from 2012 (Kayvon's 15-418 at CMU, a wonderful class), so it's been a while.

Oh good, I'm glad we did mention this!

One of the authors here:

Yes you are right, you should not replace grep for one off regexes due to the latency of the io operations. As far as I recall, memory throughput however is much higher on house than on CPUs (or at least this was true in 2012). Our intended use cases for this sort of a grep were cases where you are finding many needles in enormous haystacks such as: Looking for malicious machine code in executables that you download off of the internet (virus scanning), or searching for certain genetic sequences in DNA code. I believe we discussed this in our final presentation, but perhaps we left it out of the written report.

Yes we probably should have included the numbers to show why you wouldn't want to use this instead of grep for simple tasks. I am sorry we missed it.

I enjoyed the post, but there's something that bothers me about using the name CRDT.

A CRDT is just what mathematicians (and functional programmers) call a Semilattice[1], right? In general, I find it frustrating when people make up new names for existing mathematical concepts because it deprives others from learning and seeing the big picture. Does this resonate with anyone here?

Another interesting problem slightly more interesting than a quine is writing an auto-cannibal machine (this was a homework assignment in my semester of 15-251 at CMU):

Write a function `ACM : (String -> a) -> a` aka a function that takes a string consumer as input (such as flip_upper_and_lower_cases: String -> String, or word-count String -> Int) and outputs the result of applying this transform to it's own source code.

For example if the contents of the ACM file were: `ACM(f) = print f("foo")` (note that this is clearly not a correct answer in any language)

`ACM(flip_upper_and_lower_cases)` invoked from another file should yield: 'acm(F) = PRINT F("FOO")'

(please don't post a solution publicly just in case they're still using this as homework)

I found your post very compelling. I have tried messing around with the APL derivatives (J and K and Q), but never created anything substantial. I didn't know you could view the AST like that, and it did really help in your explanation. I'm definitely going to check out an APL again! Thank you for the great post!

Don't miss the presentation linked at the bottom of the readme[1], and the browser-based IDE, Golem linked in the middle[2].

[1] https://www.youtube.com/watch?v=HnZipJOan54 [2] http://shem.io/

Certified Programming with Dependent Types (available online as well http://adam.chlipala.net/cpdt/) is also a good resource for learning Coq (note: I just started working through the material this weekend).

I've been using scm_breeze for a couple years, and it really makes me more productive with Git.

My favorite feature is that after a `gs` all the files listed are bound to sh variables $e1, $e2, etc.

For those interested in the lecture associated with these notes: https://www.youtube.com/watch?v=GNc1t6Q5Dls

This library reminds me of some of the "future" introduced in this (satirical, yet insightful) talk: https://www.destroyallsoftware.com/talks/the-birth-and-death... Discussion: https://news.ycombinator.com/item?id=7605687

This is extremely cool, by the way.

Unfortunately, not. We had a bad gradle config for a while so when we fixed that our build time jumped down from 6min incremental to 2min. However, I can tell you that I haven't noticed an increase in build time since we fixed our gradle settings which happened a few months ago and we have added code. Maybe it's a function of gradle modules (we have around 25)? If we ever spend a bunch more time trying to optimize our build time we'll write about it somewhere.

I haven't looked into it much in the past few years so it is possible the inner class overhead on Android is not significant anymore, but a few years ago it was definitely something to watch out for on Dalvik.

Again I wasn't being very clear, sorry about that: Kotlin doesn't always reify generics, but it can for functions you mark as inline if you want (it's useful!). Check out the inline function docs!

Thanks for the info! I did know that passing lambdas to Java API calls still has to instantiate an anonymous inner class, but the details about what happens in each situation are new to me (and really interesting).

I'm sorry that I didn't make it clearer in my post (I'll edit it), but the thing I really appreciate is that I can use functional methods on objects (like map, fold, filter on iterables or our monadic bind method on optionals) and pass lambdas because I know it will be inlined. The inlining -- which should always happen this particular scenario (please correct me if I'm wrong) -- makes using these methods super cheap!

We built Roll for Android ( http://tryroll.com ) in Kotlin -- we currently have ~17k lines and have been working on it since this Spring.

We wanted to iterate on a lot of the software structure we came up with for our Swift iOS app, and for a bunch of pieces we needed a powerful type system. So rather than just stick with Java -- as others have said, it's way too verbose, we started looking at alternatives. We wanted a strong type system. Scala has too much overhead for Android. Kotlin really stood out for us. This document by Jake Wharton at Square https://docs.google.com/document/d/1ReS3ep-hjxWA8kZi0YqDbEhC... made the decision easier. So we took the risk.

And we love it!

The best features:

Null type safety!

Lambdas can be inlined! No need to be afraid of anonymous inner class overhead on the map/filter/fold of iterables.

Reified generics!

Extension functions!

Single-method interfaces/classes can be represented as lambdas! aka

  view.setOnClickListener(new View.OnClickListener() {
     @Override public void onClick(View v) { /* do something */ }
  });

becomes

  view.setOnClickListener { /* do something */ }

This is great for things like RxJava.

Speaking of which, the Java interoperability is fantastic. Any Android libraries we've tried work great from Kotlin.

Using these tools, we've built a simple dependency injection framework, a handful of really useful extensions on things like T? (for example monadic bind), a hack for algebraic data types and pattern matching, and of course a fairly complex app.

Android Studio's Kotlin support is fantastic (good job JetBrains!) -- it's a pleasure to use.

I think Kotlin is totally worth using. The biggest issue for us is the build time. Our build takes anywhere from 1.5 to 6 minutes depending on how much you've changed, but I've found that the type system is strong enough that you don't have to do too many build-change a line-rebuild cycles.

We'll be starting a blog soon to talk about some of the stuff we've been doing, but if you can't wait send me a message bkase at highlig.ht if you're interested in hearing more (I love talking about this stuff)

Not my project, so I can't update the repo. Here's a simple way to see an example:

  # clone and then  
  make && ./irscc test/main.c
  open a.pdf

I like to take advantage of temporal locality. My zshrc is configured to take me to the most recent place that I have been whenever I open a new shell:

  autoload -U add-zsh-hook
  record_pwd() { pwd > ~/.cwd }
  add-zsh-hook chpwd record_pwd
  touch ~/.cwd
  cd `cat ~/.cwd`

Thanks for the advice. As soon as we get this project to run successfully on CUDA 5, we'll update the finalreport document with the entire-application performance numbers (hopefully before the end of tomorrow).

Well I woke up to a nice surprise!

Since people seem really interested in this, mburman and I are going to spend the day fixing up this project.

This was a final project for 15-418 in Spring of 2012 (that was a great class). We need to update it for the newer versions of CUDA, and we'll probably clean up some of our code since we're both better programmers now.

Pull-requests always welcome!