From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 15E9C8239C; Tue, 26 Dec 2017 15:03:57 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=chan.ngo2203@gmail.com; spf=Pass smtp.mailfrom=chan.ngo2203@gmail.com; spf=None smtp.helo=postmaster@mail-qk0-f178.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of chan.ngo2203@gmail.com) identity=pra; client-ip=209.85.220.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="chan.ngo2203@gmail.com"; x-sender="chan.ngo2203@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of chan.ngo2203@gmail.com designates 209.85.220.178 as permitted sender) identity=mailfrom; client-ip=209.85.220.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="chan.ngo2203@gmail.com"; x-sender="chan.ngo2203@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-qk0-f178.google.com) identity=helo; client-ip=209.85.220.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="chan.ngo2203@gmail.com"; x-sender="postmaster@mail-qk0-f178.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ACnBL4BCkd53Vk7q6OPRAUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPX5pMbcNUDSrc9gkEXOFd2Cra4c0qyO6+jJYi8p2d65qncMcZhBBVcuqP?= =?us-ascii?q?49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6?= =?us-ascii?q?JvjvGo7Vks+7y/2+94fcbglUmTaxe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfO?= =?us-ascii?q?pWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnM?= =?us-ascii?q?VhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0iS?= =?us-ascii?q?cHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRsReVyJBDI2y?= =?us-ascii?q?bIUBEvQPMvpDoobnu1cDtwGzCRWwCO7tzDJDm3/43bc90+QkCQzJ0xYvH9QTu3?= =?us-ascii?q?nKrNX6LqESWv2twqnHyjXIcvRb1iv96IfSdBAtu/eMXb13ccbP10UjCw3Ig06f?= =?us-ascii?q?qYzgJTyV1+ANv3KH4OpnUOKikmgqoBx/rDiow8cjkIjJhoQNx1DA9CV52Zs1Jd?= =?us-ascii?q?ylR056fd6lEIJctyWAOItwTcMuWWZouDw1yrEetp67fTQKyJQ6xxHEcfCHco+I?= =?us-ascii?q?7grsVOaQPTd4hG9ld6mlixmu9kigz+vxXdS33lZStidJjMXAu3QX2xHQ6sWLUO?= =?us-ascii?q?Vx8lm91TqVygze6OJJLEYpnqTBMZEh2KQ/lp8LvETDACD2nEL2gbeTdko+++io?= =?us-ascii?q?7/3rYqzlppOALoN0hBzyP6Ytl8ClDuQ4NQ8OX2ef+euizrHs4Ur5QLBSgv03lK?= =?us-ascii?q?nWrozaKNwFqqKlBwJZyIUu5halAzu4ztgUgWMLIE9HdR+El4TpPkvBIPH8Dfex?= =?us-ascii?q?mVSslzJryujaMb3hGJrNKGLPkLHufbZ69UJQ1hY/wN5E6pJbD7EOOvPzWkvruN?= =?us-ascii?q?PECR85NhS4w/z7B9VlyoMeRWWPD7eFP6zItF+I4vsjI+2NZI8OpDbwMOMl5v7r?= =?us-ascii?q?jX8hg1ARZ6ip3Z0NaHC5BPtqOUuZYWD0iNcbDWgKphY+TPDtiFCaVj5ce2y9X6?= =?us-ascii?q?c45j0iCoKmCpzMRpu2jbya3Ca7G4VWaXpcBlCNF3fobYSEVO0WZCKcOM8y2gAD?= =?us-ascii?q?AIagRpNp8Rzm4BH7xqZjN7qJ0iIdvJPnktNy4ruAuws18GlKBsLV+GGESSlSkW?= =?us-ascii?q?RAEzQ21aY5p0N6kA3bioB3hvVZEZpY4PYfAVRyDoLV0+EvU4O6YQnGZNrcDQ/+?= =?us-ascii?q?Gtg=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DVAQCTVUJaf7LcVdFdGgEBAQEBAgEBA?= =?us-ascii?q?QEIAQEBAYJKgVp0FBMHg39jJDKXfIIBiH+FVIprCiOFGAKETAdDFAEBAQEBAQE?= =?us-ascii?q?BAQESAQEJCwsIJjGCOCQBgkYBAQEBAQEBIx0BGx0BAwELBgULDSoCAiEBAREBB?= =?us-ascii?q?QEcBhOKFQEDDQgQmmRAjBCCBQUBHIMLBYNYChknDVmCNQEBAQEBBQEBAQEBAQE?= =?us-ascii?q?BGAIGEoN6ghKGbYJrLRcBgVpBgmqCZQWBLQEBAZIChi+JLjMIAQGBZIYfiDSEf?= =?us-ascii?q?oIXhhaLUI0kPoVygxsUBSCBFzaBcUwjUjJSgSUJghIqDxyCBSM3AYd9gkkBAQE?= X-IPAS-Result: =?us-ascii?q?A0DVAQCTVUJaf7LcVdFdGgEBAQEBAgEBAQEIAQEBAYJKgVp?= =?us-ascii?q?0FBMHg39jJDKXfIIBiH+FVIprCiOFGAKETAdDFAEBAQEBAQEBAQESAQEJCwsIJ?= =?us-ascii?q?jGCOCQBgkYBAQEBAQEBIx0BGx0BAwELBgULDSoCAiEBAREBBQEcBhOKFQEDDQg?= =?us-ascii?q?QmmRAjBCCBQUBHIMLBYNYChknDVmCNQEBAQEBBQEBAQEBAQEBGAIGEoN6ghKGb?= =?us-ascii?q?YJrLRcBgVpBgmqCZQWBLQEBAZIChi+JLjMIAQGBZIYfiDSEfoIXhhaLUI0kPoV?= =?us-ascii?q?ygxsUBSCBFzaBcUwjUjJSgSUJghIqDxyCBSM3AYd9gkkBAQE?= X-IronPort-AV: E=Sophos;i="5.45,460,1508796000"; d="scan'208,217";a="306919706" Received: from mail-qk0-f178.google.com ([209.85.220.178]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 26 Dec 2017 15:03:55 +0100 Received: by mail-qk0-f178.google.com with SMTP id a8so6117654qkb.8; Tue, 26 Dec 2017 06:03:55 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=TVo3gHBsNUucQ5gvrZrQn32Omh90AMfZDjrPWZg1WPc=; b=AlSy7pZu8zVRdWf/hON3MXU7ItJAj/Zt6yKp8uLdqodH+RzkFo6b9mWH2nQWYefskP Jf7F3QmUrSFOnfrCRYy8kIHtQg6CY3JT/NtSDQMOVl57Ovo2L1FFP3+rxRbVvtXKe8zs GR+zJJUoBusrHJDgrf+uw3lzUBUiShx/d3z2DvRjTkS9pLhtxMzYJZ2+srLVCaXsJrn2 tfg01OjRM6lCX3YAZVaxZL6WKt+ZSE+vcJEdlYboxDzBxg0c58HB1Ju2QhqF00nk3hHI kQ0OjNR+E0YhAFZt/krkbDTEGUE6oqX9UVCnJpRoCB4xuqQhpryluI7YN+80stTrszbY t6Rw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=TVo3gHBsNUucQ5gvrZrQn32Omh90AMfZDjrPWZg1WPc=; b=Jx5sWkBbJk3WQU1PLoa+iN9pPL6rkm1blwBASWWDUoN7iffiBYNqGVE0Nr5HtFwtZo Jdizt8fMWB/EoJjNoIoS16OKo2J5Elme4ATX+O6hFsrIwFAeWcPL92FOt91ixMvWuyqN Lz0rEZe0/hhUrWGdvwhU0hOvmyOkazmUWwRSc3OsZyytCL90GQyptoDPyWGE2qLB2uTc xW1a08sb57X46Nci/Mgn41i5uFdHVbJzTylOgqc6WqBYw3WHOJVss6fB/5E6yJ1/zpng kvtAxcpTjrecRVmaWmfkkjkow5gO6zLSxwxpMSm3wF0M8dVDqxZT/M33hpRTLqsWiKnk 7ejQ== X-Gm-Message-State: AKGB3mJ72IEPiN6azfHNPO9F3qgyYqbqNHLu0Z/t8fQixb3x5YXKpkjv +YYWbu6AgKCgeTp6H/FHswi0VaEWMEHShLKQYA== X-Google-Smtp-Source: ACJfBovryjDyKPikNFHW2sKC22JpYNlpDzGQPkywHP3Gj2FP/jjedj3yH0BICiTzrXxQwAP47jJdPGbxmVy9XEgCm4E= X-Received: by 10.55.52.138 with SMTP id b132mr8101962qka.126.1514297034586; Tue, 26 Dec 2017 06:03:54 -0800 (PST) MIME-Version: 1.0 Received: by 10.200.66.154 with HTTP; Tue, 26 Dec 2017 06:03:53 -0800 (PST) In-Reply-To: References: From: Van Chan Ngo Date: Tue, 26 Dec 2017 09:03:53 -0500 Message-ID: To: Viet Le Cc: Arthur Breitman , OCaml Mailing List , ocaml-jobs@inria.fr Content-Type: multipart/alternative; boundary="001a11490184d4bd5605613ec074" Subject: Re: [Caml-list] Blockchains in OCaml --001a11490184d4bd5605613ec074 Content-Type: text/plain; charset="UTF-8" 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 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 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 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 > --001a11490184d4bd5605613ec074 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Viet,

I did not work on the formaliz= ation of EVM a while ago due to other work=C2=A0
(automatic resou= rce bound analysis for probabilistic programs https://channgo2203.github.io/pdfs/cmutr02.pd= f)
The following is the implementation (not completed) on Git= hub.

However, we are wo= rking on the other aspect of EVM code analysis. We want to statically infer= an upper-bound on the amount of gas=C2=A0
consumption for all in= puts (input arguments and storage configurations). This analysis is based o= n our previous research on resource bound=C2=A0
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=C2=A0
more con= venient to infer upper-bound on gas consumption at Solidity source code pro= vided that we have a good gas consumption model for=C2=A0
Solidit= y 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 OC= aml but I found some interesting links:



<= div>
<= div>

I= would like to know more if anyone has more information.

Thanks,
Viet

On 10 October 2016 at 15:00, Van Ch= an 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 Vir= tual Machine (EVM, the running environment of smart contracts) in Coq.

Best,
-Chan

<= br>
On Oct 5, 2016, at 11:59 PM, A= rthur Breitman <a= rthurb@tezos.com> wrote:

If you find this intriguing and enjoy working in O= Caml, 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 b= e interested in proving the correctness of some aspects of the protocol or = sponsoring research in the field in general (within our modest means).


<= br clear=3D"all">

--
Kind regards,
=
Viet

--001a11490184d4bd5605613ec074--