From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 2C0D68239C; Wed, 27 Dec 2017 16:41:35 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vietlq85@gmail.com; spf=Pass smtp.mailfrom=vietlq85@gmail.com; spf=None smtp.helo=postmaster@mail-qk0-f171.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of vietlq85@gmail.com) identity=pra; client-ip=209.85.220.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="vietlq85@gmail.com"; x-sender="vietlq85@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of vietlq85@gmail.com designates 209.85.220.171 as permitted sender) identity=mailfrom; client-ip=209.85.220.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="vietlq85@gmail.com"; x-sender="vietlq85@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-f171.google.com) identity=helo; client-ip=209.85.220.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="vietlq85@gmail.com"; x-sender="postmaster@mail-qk0-f171.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Az0JoixQJy2OIesBLYrGIf7TIDNpsv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa6zZh2N2/xhgRfzUJnB7Loc0qyK6/mmATRIyK3CmUhKSIZLWR4BhJ?= =?us-ascii?q?detC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+?= =?us-ascii?q?KPjrFY7OlcS30P2594HObwlSizexfa5+IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf?= =?us-ascii?q?5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbD?= =?us-ascii?q?VwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0li?= =?us-ascii?q?gIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRDDYOy?= =?us-ascii?q?b4UBAekPM/tGoYbhvFYBtweyCBO2Ce/z1jNFhHn71rA63eQ7FgHG2RQtEN0PsH?= =?us-ascii?q?vKsNX+KaEcXv6ox6TP0zXDbu1Z2Sv56IjRcR0soeqBXb11ccXLyEkvExnJgUmX?= =?us-ascii?q?qYzgJj6Y0PkGvWac7+plT+2vimgnphlwozexwMcskpPJhoUJylDD6Sp5x4I1Kc?= =?us-ascii?q?ekR058ZN6oCJ9QtyCDN4trQ8MtXmBouDo6y7EfvZ60Zi4KyJs9yx7YcfyHfJCE?= =?us-ascii?q?4h3iVOaNITd4mWlqdKi+hxa16USgxez8VtW00FZXtSVJiMXDtncI1xHV98OJSe?= =?us-ascii?q?N981+/1TqT0w3f8OJJLEAumabFNZIt3qQ8mocRvEjeGCL9hV/4g7WMdko+/+il?= =?us-ascii?q?8+Tnbavipp+bL4J0jxvxMqUqmsCmGOQ4MRQCU3GV+eih1rDv4Ff1QLpNjv0xna?= =?us-ascii?q?nZtI7VKd4Hqa6+Bg9Zyocj6xChADe6yNkUg2ULIVZfdB+Ej4XlIU/CLO7kAful?= =?us-ascii?q?nlihkipny+jDPrL7A5XNKnbDkK3mfbZ480Nc1gszws5D55JQE7EMI/L+V1T+tN?= =?us-ascii?q?zdFBA5Mgi0z/z7B9V604MSQXiPDbOBMKPOrV+I4foiLPWWa48QvDbxMvwl5//1?= =?us-ascii?q?jX8lglIdZqmo3Z4PaH+iBPhmIkOZYWDtgtgbC2sKsBA+RvTwiFKeST5Te2qyX6?= =?us-ascii?q?Uk6zE8FI2pF4LDRoS0jLyD2ye0BYZWa3tdClGMFHfob5+LV+0NaCKUOM9hkyYL?= =?us-ascii?q?WaKvS487hlmSs1rEwrwvBerd/GU+upWrgNN17uuVkx41r2YsVOyS1miMSyd/mW?= =?us-ascii?q?ZeFBEs26Uqn01w1h+n3OAsnf1VCdhKt65hXQIzNJqaxOt/XYOhEjndd8uEHQ71?= =?us-ascii?q?Cu6tBis8G5dom4cD?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0B+AQDuvUNahqvcVdFdGgEBAQEBAgEBA?= =?us-ascii?q?QEIAQEBAYJKgVp0FBMHg3+BBzKYAIIBiH+FVIprCiOFGAKETgdDFAEBAQEBAQE?= =?us-ascii?q?BAQESAQEBCAsLCCgvgjgkAYJGAQEBAQEBASMdARsdAQMBCwYFCw0qAgIhAQERA?= =?us-ascii?q?QUBHAYTG4l6AQMNCBCaAECMEIIFBQEcgwsFg1gKGScNWVGBZAEBAQEBBQEBAQE?= =?us-ascii?q?BAQEBARcCBhKDeoIShm2Cay0XAYFaQYJqgmUFgS0BAZgyiS4zCAEBgWQKhhWIN?= =?us-ascii?q?IR+gheGFotQjSQ+hXKDGxQFIIEXNoFxb1IyUoElCYISKg8QDIFnQTcBhzaCSQE?= =?us-ascii?q?BAQ?= X-IPAS-Result: =?us-ascii?q?A0B+AQDuvUNahqvcVdFdGgEBAQEBAgEBAQEIAQEBAYJKgVp?= =?us-ascii?q?0FBMHg3+BBzKYAIIBiH+FVIprCiOFGAKETgdDFAEBAQEBAQEBAQESAQEBCAsLC?= =?us-ascii?q?CgvgjgkAYJGAQEBAQEBASMdARsdAQMBCwYFCw0qAgIhAQERAQUBHAYTG4l6AQM?= =?us-ascii?q?NCBCaAECMEIIFBQEcgwsFg1gKGScNWVGBZAEBAQEBBQEBAQEBAQEBARcCBhKDe?= =?us-ascii?q?oIShm2Cay0XAYFaQYJqgmUFgS0BAZgyiS4zCAEBgWQKhhWINIR+gheGFotQjSQ?= =?us-ascii?q?+hXKDGxQFIIEXNoFxb1IyUoElCYISKg8QDIFnQTcBhzaCSQEBAQ?= X-IronPort-AV: E=Sophos;i="5.45,466,1508796000"; d="scan'208,217";a="307001900" Received: from mail-qk0-f171.google.com ([209.85.220.171]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 27 Dec 2017 16:41:33 +0100 Received: by mail-qk0-f171.google.com with SMTP id q14so34054689qke.7; Wed, 27 Dec 2017 07:41:33 -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=cSfI+s9CKz6FTqetapTwIJ9YqLUmQaaekIvB9LdDiaQ=; b=dT8PkPi7j/+KWVYP/4gwOVOYKLSt8NBB8ONiXY+RtcuwQPViKh3i4Bgtw+6S+9QprA FBvcrIGFnXLTB/KvBTYYfPiH36HZ22Pn151mwZ/cykkzQlKEA5a2k8lXKnJnmz3uRRLX sf8J96wyKRMCDup2XBttgud8l+iixHrXEElpq3Xnl++GH7zCA48zdnbVTVR9V92a57ob Z7RdixtPHLnDl+LRV52NILIQgkdd3zdKFUCtO8Wj7+5HICNgSE+3Mj02a98KHrUVYn1Q WSMgrE/MD0giqUnPwJ70WCaC0F265CAZXIdRV7W6xXMRl9dDCn/fD0zFJwHZVYYPBhhr 02VA== 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=cSfI+s9CKz6FTqetapTwIJ9YqLUmQaaekIvB9LdDiaQ=; b=QpnuspUAUbED/ktUrn+sr/g9SGJQNGw6FkmwiwmhYNhvAmZ870wigtB9xNLi24UK1x jnFQFobaLVbusu52CK2c4zJZ2sfeIJW8RVNRolS4NdRm/beqJ+Sx5jf8qMiNejZSDBuB gCbR3Xih4l4gKzQyurCfuKIm9Kck7gFIiavqmMUdmeNipAUwIVQqADe4RN80FICgFNGy F4TecX9SA1YPxQP3jQg+Zd/RyEQ4kGFqs4NaRqUsosAtvU6lPNQp1R6bzmuTeS4H7R/w nQfkuvZ4hZTotARjHkZ4ydpxmukZsFzy8+tMesE7rexELXfl3GY6hgZMd5mfY2bHvjIH 2RHA== X-Gm-Message-State: AKGB3mKoUnka27PmFtdqLQEijmDq3bRYv93ajKXieQYVPSqC3NJ4oGFN kxH9r8mcRTERLhsbWScdnjS02ocsC7O+JcZUOq7Jd6pi X-Google-Smtp-Source: ACJfBou0T4lfNZ/hidcCqrUjyLnZbDJj3kdpIK1M4dHncwpkrc6K1P2+UhBqg2tI2JBAORO/UsWwwJo1g6mWyt8bsAM= X-Received: by 10.55.106.131 with SMTP id f125mr36297812qkc.88.1514389292581; Wed, 27 Dec 2017 07:41:32 -0800 (PST) MIME-Version: 1.0 Received: by 10.140.84.148 with HTTP; Wed, 27 Dec 2017 07:41:32 -0800 (PST) In-Reply-To: References: From: Viet Le Date: Wed, 27 Dec 2017 15:41:32 +0000 Message-ID: To: Van Chan Ngo Cc: Arthur Breitman , OCaml Mailing List , ocaml-jobs@inria.fr Content-Type: multipart/alternative; boundary="001a114fe758d609790561543bea" Subject: Re: [Caml-list] Blockchains in OCaml --001a114fe758d609790561543bea Content-Type: text/plain; charset="UTF-8" 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 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 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 >> > > -- Kind regards, Viet --001a114fe758d609790561543bea Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thanks Van Chan for sharing.

I also fou= nd a solution that automatically computes the gas used by breaking down int= o basic computations. They are Zen Protocol:=C2=A0https://www.zenprotocol.com . They use F* that is very c= losely related to OCaml/F# to achieve their goal. So if you want to find up= per-bound for EVM, I think their whitepaper is a good start.

=
Regards,
Viet

On 26 December 2017 at 14:03, Van Chan Ngo <ch= an.ngo2203@gmail.com> wrote:
Hi Viet,

I did not work on the formal= ization of EVM a while ago due to other work=C2=A0
(automatic res= ource bound analysis for probabilistic programs https://channgo2203.githu= b.io/pdfs/cmutr02.pdf)
The following is the implementati= on (not completed) on Github.

However, we are working on the other aspect o= f EVM code analysis. We want to statically infer an upper-bound on the amou= nt of gas=C2=A0
consumption for all inputs (input arguments and s= torage configurations). This analysis is based on our previous research on = resource bound=C2=A0
analysis for both imperative and functional = programs.

We translate EVM byte-code into a kind o= f control flow graph (CFG). However, due to the unstructured and low level = of EVM, I suppose it is=C2=A0
more convenient to infer upper-boun= d on gas consumption at Solidity source code provided that we have a good g= as consumption model for=C2=A0
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 ye= ar 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 implemen= tations in OCaml but I found some interesting links:

https://github.com/LaurentMazare/btc-ocaml
<= div>

= 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 abou= t this project.

FYI, a related work, we are in pro= gress to formalize the Ethereum Virtual Machine (EVM, the running environme= nt of smart contracts) in Coq.

Best,
-Ch= an


=
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 s= ide 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).<= /div>




--
Kind regards,
Viet




--
=
Kind regards,
Viet
--001a114fe758d609790561543bea--