Re: [Caml-list] Blockchains in OCaml

[Viet Le <vietlq85@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 3058 bytes --]

Thanks Van Chan for sharing.

I also found a solution that automatically computes the gas used by
breaking down into basic computations. They are Zen Protocol:
https://www.zenprotocol.com . They use F* that is very closely related to
OCaml/F# to achieve their goal. So if you want to find upper-bound for EVM,
I think their whitepaper is a good start.

Regards,
Viet

On 26 December 2017 at 14:03, Van Chan Ngo <chan.ngo2203@gmail.com> wrote:

> Hi Viet,
>
> I did not work on the formalization of EVM a while ago due to other work
> (automatic resource bound analysis for probabilistic programs
> https://channgo2203.github.io/pdfs/cmutr02.pdf)
> The following is the implementation (not completed) on Github.
> https://github.com/channgo2203/fevm
>
> However, we are working on the other aspect of EVM code analysis. We want
> to statically infer an upper-bound on the amount of gas
> consumption for all inputs (input arguments and storage configurations).
> This analysis is based on our previous research on resource bound
> analysis for both imperative and functional programs.
>
> We translate EVM byte-code into a kind of control flow graph (CFG).
> However, due to the unstructured and low level of EVM, I suppose it is
> more convenient to infer upper-bound on gas consumption at Solidity source
> code provided that we have a good gas consumption model for
> Solidity language constructs.
>
> Best,
> -Van Chan
>
>
>
>
> On Mon, Dec 25, 2017 at 8:28 AM, Viet Le <vietlq85@gmail.com> wrote:
>
>> Hi all,
>>
>> Only one year after this message, I found interest in building a
>> blockchain and smart contracts in OCaml. May I know how far is the EVM
>> formalisation in Coq?
>>
>> There aren't many materials / blockchain implementations in OCaml but I
>> found some interesting links:
>>
>> https://github.com/LaurentMazare/btc-ocaml
>>
>> http://www.liquidity-lang.org/
>>
>> https://github.com/tezos/tezos
>>
>> https://github.com/pirapira/eth-isabelle
>>
>> https://github.com/pirapira/ethereum-formal-verification-overview
>>
>> I would like to know more if anyone has more information.
>>
>> Thanks,
>> Viet
>>
>> On 10 October 2016 at 15:00, Van Chan Ngo <chan.ngo2203@gmail.com> wrote:
>>
>>> Hi Arthur,
>>>
>>> It is interesting to implement blockchains in functional language like
>>> OCaml. I am happy to hear more about this project.
>>>
>>> FYI, a related work, we are in progress to formalize the Ethereum
>>> Virtual Machine (EVM, the running environment of smart contracts) in Coq.
>>>
>>> Best,
>>> -Chan
>>>
>>>
>>> On Oct 5, 2016, at 11:59 PM, Arthur Breitman <arthurb@tezos.com> wrote:
>>>
>>> If you find this intriguing and enjoy working in OCaml, please reach
>>> out: we're hiring! If you lean on the academic side and have experience
>>> with formal verification, reach out as well! We'd be interested in proving
>>> the correctness of some aspects of the protocol or sponsoring research in
>>> the field in general (within our modest means).
>>>
>>>
>>>
>>
>>
>> --
>> Kind regards,
>> Viet
>>
>
>


-- 
Kind regards,
Viet

[-- Attachment #2: Type: text/html, Size: 6236 bytes --]