Looks pretty neat. As someone who hasn't followed Bitcoin for the last 5 years, what are some things people have built with smart contracts? Also, are Bitcoin smart contracts Turing Complete and suffer the same gas issue as ETH where you don't know how much gas you need?
Bitcoin Script is non-turing-complete in nature(so no gas issue!), so does Bithoven. Bithoven doesn't extend Bitcoin Script Opcodes(which requires consensus upgrade on the protocol), but inherit and abstract for the expressiveness. Moreover, it supports static analysis to cache some known security bugs.
I omitted one detail in the original post: Bithoven uses an LALR parser generator (Lalrpop) to strictly define the formal grammar and avoid ambiguities when parsing to the AST!
Quick suggestion - adding simulators for checking all spend paths would add comfort. A lot of comfort. I understand you're doing static analysis on construction, which is great; more safety would be awesome too.
If I missed that you have these, then, I doubly love this! :)
Yes, simulator definitely would! Actually I'm planning to add input constructor or simulator to generate safe symbolic/static inputs for users, and simulate with symbolic script engine to validate even stricter.
As it might require the Bitcoin Script interpreter (with symbolic execution for things like signature), I left it as a near future work.
I've researched the previous works surely, and actually contributed miniscript(the most notable one in industry AFAIK) quite a lot(https://github.com/rust-bitcoin/rust-miniscript). Contributions to the previous work has actually motivated me to research and implement this. As you may know, miniscript, while could be safer as restricted policy lang, is not really expressive enough to express many bitcoin opcodes(e.g. + and - op), and really hard to understand and write for dev not familiar with Bitcoin Script.
I understand that Bitcoin Script itself is pretty limited(no mul/div, no bit-operation, no loop), but there must be safe and expressive language as it's standard for UTXO blockchain including bitcoin. The security bug happening because of primitive and hard-to-understand Bitcoin Script could be as severe issue as other advanced programming language bug, as it's directly related to money! Lack of expressiveness also does discourage the possible smart contract application on Bitcoin, which has a high potential value considering mega-economy of Bitcoin.
Bithoven has added expressiveness(and I think it does make a sense for real world impact), and also tried to catch severe agonizing money loss bug with a static anaylzer.
Looks pretty neat. As someone who hasn't followed Bitcoin for the last 5 years, what are some things people have built with smart contracts? Also, are Bitcoin smart contracts Turing Complete and suffer the same gas issue as ETH where you don't know how much gas you need?
Bitcoin Script is non-turing-complete in nature(so no gas issue!), so does Bithoven. Bithoven doesn't extend Bitcoin Script Opcodes(which requires consensus upgrade on the protocol), but inherit and abstract for the expressiveness. Moreover, it supports static analysis to cache some known security bugs.
Even if limited nature, there are many applications of smart contract like hashed-time lock contract, inheritance and multisig contract! You can see examples: https://github.com/ChrisCho-H/bithoven/tree/main/example
I would be glad to anyone who would add example bithoven code!
I omitted one detail in the original post: Bithoven uses an LALR parser generator (Lalrpop) to strictly define the formal grammar and avoid ambiguities when parsing to the AST!
I love this! Thanks for making it.
Quick suggestion - adding simulators for checking all spend paths would add comfort. A lot of comfort. I understand you're doing static analysis on construction, which is great; more safety would be awesome too.
If I missed that you have these, then, I doubly love this! :)
Yes, simulator definitely would! Actually I'm planning to add input constructor or simulator to generate safe symbolic/static inputs for users, and simulate with symbolic script engine to validate even stricter. As it might require the Bitcoin Script interpreter (with symbolic execution for things like signature), I left it as a near future work.
I don't think it makes any sense except for fun, Bitcoin scripts are pretty limited and there are a lot of previous work [1][2][3][4][5].
[1] https://bitcoin.sipa.be/miniscript/
[2] https://min.sc/
[3] https://docs.scrypt.io/
[4] https://github.com/sapio-lang/sapio
[5] https://github.com/ivy-lang/ivy-bitcoin
I've researched the previous works surely, and actually contributed miniscript(the most notable one in industry AFAIK) quite a lot(https://github.com/rust-bitcoin/rust-miniscript). Contributions to the previous work has actually motivated me to research and implement this. As you may know, miniscript, while could be safer as restricted policy lang, is not really expressive enough to express many bitcoin opcodes(e.g. + and - op), and really hard to understand and write for dev not familiar with Bitcoin Script.
I understand that Bitcoin Script itself is pretty limited(no mul/div, no bit-operation, no loop), but there must be safe and expressive language as it's standard for UTXO blockchain including bitcoin. The security bug happening because of primitive and hard-to-understand Bitcoin Script could be as severe issue as other advanced programming language bug, as it's directly related to money! Lack of expressiveness also does discourage the possible smart contract application on Bitcoin, which has a high potential value considering mega-economy of Bitcoin.
Bithoven has added expressiveness(and I think it does make a sense for real world impact), and also tried to catch severe agonizing money loss bug with a static anaylzer.
Docs: https://bithoven-lang.github.io/bithoven/docs/