saurabh20n

We are looking for people who want to play around with constraint solvers. As others in this thread have mentioned, the vanilla Sudoku is not hard to really need constraint solvers; a generalized version would. We don't expect people to have backgrounds in program synthesis, but constraint solving is a start.

That said, it is just a fun problem. PTime specialized solutions are even more intriguing.

This page was just a fun exercise; seems to have missed communicating fully how we use synthesis. My bad.

You are right about about "2." and part of "3.". For "2." yes, the smart contracts are indeed simpler (small code, gas limits, closed systems). So we can skip some major hurdles that more general techniques need -- case in point the FB abstract interpretation framework Sparta here yesterday. For "3." we use Z3 (as should everybody :)!) but the target language for synthesis is Solidity. [ Hope you didn't mean Solidity is a DSL, coz that would be a generous interpretation of that word. ]

The initial spec is another smart contract (call it IN), so code and not a formal constraint. We synthesize another smart contract (call it OUT), such that the combination (IN + OUT) behaves well. See work on synthesizing program inverters for the background ideas (http://saurabh-srivastava.com/pubs/pldi11-pins.pdf)

You are absolutely right. Punching "extra holes" in puzzles of certain hardness should make backtracking not as viable. But we'll loose the unique solution property.

Might make it more interesting? And maybe even bias it towards human-abilities. I think intuitively we're better at solving when the possibilities are more than 1 (just a conjecture.)

Trail of bits is not building anything in program synthesis.

About the benchmarks, SMT-LIB has had my instances for close to a decade now :) [1,2] We are now generating non-bitvector benchmarks, and maybe in the Fall we will submit newer instances.

Back in the day, I was foolish enough to implement my own (bitvector) solver. Hoping to outcompete with the assumption that I could encode heuristics informed by the domain (i.e., synthesis-specific). Turned out Z3's "general" heuristics were just faster. You could say, I let Nikolaj and Leonardo take it from there. For completeness, I also did experiment with a bunch of other solvers that were considered good at the time [3]. (Have to caveat with the fact that CVC3, now CVC4, has always been on my list of future-to-try.)

---

[1] VS3: QF_BV (bitvector benchmarks) https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B... -- apologies for the unimaginative name. VS3 stands for "(V)erification and (S)ynthesis using (S)MT (S)olvers"

[2] Example SMT instance: https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_B...

[3] Engineering for synthesis using SMT solvers: Chapter 6 of PhD: http://saurabh-srivastava.com/pubs/saurabh-srivastava-thesis...

The below were written for a semi- or non-technical audience, and only address your curiosity tangentially, but better than nothing:

* Program synthesis overview: https://medium.com/@vidiborskiy/software-writes-software-pro...

* Program synthesis to make smart contract security more accessible: https://medium.com/@vidiborskiy/program-synthesis-smart-cont...

* Synthetic Minds (that is us): https://synthetic-minds.com/

You can help by telling me what questions would be most informative to answer. Promise to write a post addressing them directly.

Z3 is amazing. I have been working with it since 2007. We are now building program synthesizers using it. Having a solid system to do the heavy lifting is a life saver.

Agree with the scale. But do you mean the compilers toolchain is the largest/safest; or the overall C++ codebase. No questions about the latter, but would be surprised if you meant the former.

Out of curiosity: if not the language platform team, then which team does PL research? My email is in my profile of you'd rather ping there.

Honest question: does the current Google have the environment to innovate on the next generation of compilers/PL/program synthesizers?

I would have definitely said yes back in the day; but not so sure now.

(Admittedly might be biased. I'm the founder of Synthetic Minds. We're building program synthesizers; basically all compilers work: https://news.ycombinator.com/item?id=19059922)

Synthetic Minds (YC S18) | SF + Seattle | $120k+ | First 5 engineers: commensurate equity | ONSITE, Full Time

The ideal candidate has a master/phd in systems, compilers, programming languages, or distributed systems; but never gets to use it in their day job. Synthetic Minds will allow you to leverage your technical chops.

Synthetic Minds is building program synthesizers, i.e., automation that can write code. We have a system in production that reads/writes smart contracts in Ethereum's Solidity language, and we use it to ensure our customer's code is secure and correct. Eventually, we plan on going far beyond smart contracts. Think of what we are building as a compiler that takes code and translates it to theorem proving, so that we can build automation that can understand code almost as close to a human. If it can understand code, with sufficient compute it can even “synthesize” it.

In Oct 2018, we raised a $5.6M seed round from Y Combinator, Khosla Ventures and Pantera Capital [6]. We have paying customers and a backlog waiting to be on-boarded. The team is heavily experienced. This is the founder’s second startup and they have a PhD in the area. The 1st employee was the first hire at Parse (YC S11) and has 10 yrs at Google. We aim to be a 10-15 person all-engineering team in 2019.

Roles/Openings (see [1]): # Software engineer: Systems/infrastructure — You’ll be working on distributing heavy CPU processes on AWS. Making sure processes run reliably over many days. Ensure robustness of the infrastructure across node/process/memory/algorithm failures.

# Software engineer: Compilers/verification/synthesis — You’ll be working on developing new algorithms that analyze and generate code [2]. You’ll identify when an engineering solution is needed (i.e., throw across a cluster of machines), or when an algorithmic improvement is required. You might even play with the Z3 theorem prover [3]. And if you’re really into it, you can improve Z3.

# Software engineer: Smart contracts — You’ll be working on the “front-end of the compiler”, which reads in smart contracts languages (e.g., Solidity) and makes it accessible to the backend (the part that does semantic analysis). Desire to work at the compiler level of smart contracts is required, e.g., see [4] — experience in writing smart contracts is easily acquired as a side effect.

Contact: saurabhs@synthetic-minds.com - Saurabh, Founder

[1] Synthetic Minds Jobs: https://synthetic-minds.com/pages/jobs.html

[2] Program synthesis: https://medium.com/@vidiborskiy/software-writes-software-pro...

[3] Z3 Theorem Prover: https://github.com/Z3Prover/z3

[4] Solidity AST: https://github.com/ethereum/solidity/blob/develop/libsolidit...

[5] Solidity smart contracts: https://solidity.readthedocs.io/en/v0.4.21/solidity-by-examp...

[6] Forbes funding article: https://www.forbes.com/sites/darrynpollock/2018/10/22/invest...

As some other people have pointed out, you have to pick the domain and application. Airbus controllers (abstract interpretation [1]), Microsoft software driver verification (SLAM model checker [2]) were ones where formal methods found use in the pre-2010 era. Since then, the domain has led to work that brings Excel the capability to auto fill data [3], toy demonstrations of how synthesize programs while verifying them correct [4], verify file systems [5], and now verify and synthesize smart contract code (whose deployments are expected to be permanent) [6]. This is just a sampling. There are many of other uses.

[1] Astree http://www.astree.ens.fr

[2] SLAM SDV https://www.microsoft.com/en-us/research/project/slam/

[3] flashfill https://www.microsoft.com/en-us/research/blog/flash-fill-giv...

[4] Invariant based synthesis https://www.microsoft.com/en-us/research/wp-content/uploads/...

[5] FS verification https://www.usenix.org/conference/atc17/technical-sessions/p...

[6] Solidity verification and synthesis https://synthetic-minds.com

90% of the page at the bottom is the transcript. Right below the audio file is the time annotated transcript as well. Might have been added after you opened it: should recheck.

It would be useful to have a section: "What AI cannot do" or to be pedantic: "What the current AI techniques cannot do."

Comparison-based sorts have O(1) complexity on the size of the elements being sorted. I.e., comparison between two numbers is a single instruction assuming numbers fit within a word. Even if you assume very very large numbers then comparison would be O(k), where k is number of bits needed to represent a number. So a more accurate runtime of O(nlogn) algorithms should be O(k.nlogn).

The runtime of this algorithm is O(n.2^k).

Synthetic Minds (YC S'18) | mostly ONSITE in SF | First non-founder engineers

We're building program synthesizers, i.e., automation that can write code.

I have an MVP in production that reads/writes smart contracts (i.e., small, permanent, apps) in Ethereum's Solidity language, and use it to ensure our customer's code is secure and correct. Synthesis could eventually enable access to code for non-programmers. For now, goal is simple: My customers give me source code for their contract (= Ethereum apps, which are self-contained). I use synthesis to generate another contract/app that demonstrates any problematic interaction.

Backed by Y Combinator, Khosla Ventures and Pantera Capital. We have paying customers, with a backlog waiting to be on-boarded, and are profitable.

Ideal candidate will have a MS or PhD in program synthesis, formal methods or related fields. But also looking to fill other roles: https://synthetic-minds.com/pages/jobs.html

I'm guessing you meant McAfee for Dapps?

Yes. It should work. There's a good amount of work to be done though. :)

I don't follow what you mean by a "debugger" in this case.

Ah. I see why that was unclear.

I make multiple SMT queries. SMT solvers work well in practice, but they are solving a problem which is between NP-Complete to Undecidable (when quantifiers are involved [1]).

Also, we are using a very hand-wavy word definition "complexity of code". This is not the complexity-theory complexity, but instead the types of operations used and the looping/control structure. (In hindsight, I should have used a different word.) So 40 lines of multiple nested loops with multiple hashes being taken and multiple dynamic dispatches over addresses, will take much much longer to analyze than 40 lines of straight line arithmetic.

My tool attempts to guess the estimated runtime midway through the analysis, but there is no real way to accurately estimate the cost upfront. That is why I was saying that if it cost ~$200 for 20-50 LoC then if you accept all caveats then under wildly simplifying assumptions the 500 LoC might take 10x-25x of that cost.

[1] https://stackoverflow.com/a/10924475

Thanks!

The key distinction is building a synthesizer, not just a verifier. These systems are hard to use, and synthesized code is the key to making them accessible. Watch the demo videos. See if you agree.

On the verifier side: QSP is a protocol/marketplace for connecting people needing audits, with human auditors or free open source tools (Oyente and Mythril) [1]. My verifier is more comprehensive and future-proof at the expense of being compute intensive, as discussed on my FAQ [2].

[1] https://quantstamp.com/visual-guide-to-quantstamp

[2] FAQ: "How is this different from Ethereum's other tools ?" https://synthetic-minds.com/pages/faq.html

You sir or madam, have a devious mind :). I shall hold on to my trust in humanity for a little while longer!

If you see the demo runs on the website FAQ, that example of about 20-50 LoC cost ~$200. You can extrapolate accordingly. Now if you integrate into your CI, I am of course going to only rerun on changes (syntactic, easily checked; and hopefully semantic later.)

If you want a more precise cost analysis, shoot me an email for your specific contract.

And you are right about audits. Except a caveat: The system will by default check for global properties as well, e.g., no double spend. Again, look at the examples in the FAQ. They had no assertions in them. Yet, we find errors.

Fixed. Thanks for noticing.

Look up Nate's work [1], specifically Boomerang [2] that aims for bidirectional programming. Be crazy :)

[1] Nate Foster: http://www.cs.cornell.edu/~jnfoster/ [2] Boomerang http://www.seas.upenn.edu/~harmony/

It will be pay for use, like AWS. You fill up, and then depending on how compute-heavy your contracts are to analyze, you will be charged accordingly. Your costs will end up depending on complexity of your contracts.

Compare this to the alternatives of paying $20,000 - $500,000 for manual audits.

Your `D(K(..))` notation is better than mine. Email me, and I will send you a gift card.

What you do is solve `\exists D: \forall arr: D(K(arr)) = arr` where `arr` is an arbitrary length array/bitstream. See paper [1]. There is also really old code you can browse at the bottom of my personal page linked in profile (doesn't compile anymore coz of deprecated dependencies.)

The arithmetic analogy break down when solving. So you're not explicitly computing `I - K`, but instead letting the constraint solver pick values that satisfy the equation (hence SMT solving.) Also, you are absolutely right that there is no reason to have their structure be related to identity: But, the "damage" done by `K` is encoded in the state at the interface to `D` and `D` better undo that state to get to identity, which is what the solver would exploit.

[1] Path-based Inductive Synthesis for Program Inversion http://saurabh-srivastava.com/pubs/pldi11-pins.pdf

I get your concern about the current-state. The "dev/money" ratio needs adjustment. Market cap/ICO/yet-another-cryptocurrency is not what excites me.

I am working on a simple premise: The DAO (perpetually running, globally accessible, democratic kickstarter) would have been a good project to see succeed. It failed not because it was a bad idea, but because we rushed into it without tools like this one. Augur, Aragon, 0x, Golem, Filecoin are other projects that might be worthwhile. Also ZCash (doesn't have smart contracts yet, but you should really look into the work Ariel Gabizon and company are doing.)

You wouldn't want to write an linux kernel code without a compiler, would you? You shouldn't write immutable code without formal verifiers. Agree?

Yes. The hope is that you run this analysis as part of your development workflow. e.g., on every merge into master. Charge up like AWS and use as frequently as you need. The current alternatives involve hiring a firm for $20-500k for a manual audit that happens at the end of years long development. I will work with you to get this into your hands as soon as I can.

All great points. And I agree with you on most everything.

I care about the major complicated projects succeeding, e.g., 0x, Golem, Augur, Aragon, to name a few. They can go the DAO route, or I can do my part in helping. Help me get in touch with more projects if you're connected.

Open sourcing right off the bat will have the opposite effect. If it works at scale, we will be pitting the attackers against the developers. I would rather get this tool in the hands of developers first. I welcome other people developing the same :) - better yet: I've already developed a version, come help me make it useful for the community.

LOL. I agree. Want to take a stab at it?

I am not using Rosette, although I love the work Emina and Ras are doing to make synthesis accessible.

[ Edit: Your idea is fantastic, btw. If you can find use cases where the size of contracts is small, it'll be amazing to have synthesis from test cases. ps: Do borrow some ideas from the way Sumit solves Flashfill. ]

My system is closed source, partially because it is computationally heavy and I'll spin up a server fleet for analyses, and also because I don't want it to be used for attacks, i.e., limit use to mostly the original developers of projects.

Connect with the email on the website. I'll look at your code a little later.

Absolutely right! Which is why I am connecting directly with the project developers. Also, I specifically built it to run over Solidity source code. As opposed to EVM bytecode like other tools. Only 1% of contracts have their Solidity code public on Etherscan. Making this accessible to 100% of the original developers and only 1% of attackers, should limit it to white-hat uses.