4 ms·
TLDR : we use a solver to go from a formal constraint specification to an Ethereum smart contract So 1. the initial specification is still a formal const
by yazr 8y ago
TLDR : we use a solver to go from a formal constraint specification to an Ethereum smart contract
So
1. the initial specification is still a formal constraint
2. the domain complexity is low
3. Use well known solvers to generate code in a DSL
- saurabh20n 8y agoThis 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 http://saurabh-srivastava.com/pubs/pldi11-pins.pdf)
- yazr 8y agoThanks for the explanation. Program synthesis is HARD, and we may never solve it, so any progress on this is great to read about. Good luck with this.