Re: [Caml-list] Blockchains in OCaml

[Van Chan Ngo <chan.ngo2203@gmail.com>]

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

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
>

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