Deploy website - based on 5d6ecfe

formal-land · Jan 22, 2024 · 8d60fba · 8d60fba
1 parent 2121f66
commit 8d60fba
Show file tree

Hide file tree

Showing 74 changed files with 215 additions and 215 deletions.
diff --git a/404.html b/404.html
diff --git a/assets/js/main.31e3dc13.js b/assets/js/main.31e3dc13.js
diff --git a/assets/js/main.5b0bc398.js b/assets/js/main.5b0bc398.js
diff --git a/assets/js/main.31e3dc13.js.LICENSE.txt → assets/js/main.5b0bc398.js.LICENSE.txt b/assets/js/main.31e3dc13.js.LICENSE.txt → assets/js/main.5b0bc398.js.LICENSE.txt
diff --git a/blog.html b/blog.html
diff --git a/blog/2021/10/10/welcome.html b/blog/2021/10/10/welcome.html
diff --git a/blog/2021/10/27/verification-data-encoding.html b/blog/2021/10/27/verification-data-encoding.html
diff --git a/blog/2021/11/12/new-blog-posts-and-meetup-talk.html b/blog/2021/11/12/new-blog-posts-and-meetup-talk.html
diff --git a/blog/2022/02/02/make-tezos-a-formally-verified-crypto.html b/blog/2022/02/02/make-tezos-a-formally-verified-crypto.html
diff --git a/blog/2022/06/15/status update-tezos.html b/blog/2022/06/15/status update-tezos.html
diff --git a/blog/2022/06/23/upgrade-coq-of-ocaml-4.14.html b/blog/2022/06/23/upgrade-coq-of-ocaml-4.14.html
diff --git a/blog/2022/12/13/latest-blog-posts-on-tezos.html b/blog/2022/12/13/latest-blog-posts-on-tezos.html
diff --git a/blog/2023/01/24/current-verification-efforts.html b/blog/2023/01/24/current-verification-efforts.html
diff --git a/blog/2023/04/26/representation-of-rust-methods-in-coq.html b/blog/2023/04/26/representation-of-rust-methods-in-coq.html
diff --git a/blog/2023/05/28/monad-for-side-effects-in-rust.html b/blog/2023/05/28/monad-for-side-effects-in-rust.html
diff --git a/blog/2023/08/25/trait-representation-in-coq.html b/blog/2023/08/25/trait-representation-in-coq.html
@@ -11,11 +11,11 @@
 <script async src="https://www.googletagmanager.com/gtag/js?id=G-MQLHF4EV4J"></script>
 <script>function gtag(){dataLayer.push(arguments)}window.dataLayer=window.dataLayer||[],gtag("js",new Date),gtag("config","G-MQLHF4EV4J",{anonymize_ip:!0})</script><title data-react-helmet="true">Trait representation in Coq | Formal Land</title><meta data-react-helmet="true" name="twitter:card" content="summary_large_image"><meta data-react-helmet="true" property="og:image" content="https://formal.land/img/land-512.png"><meta data-react-helmet="true" name="twitter:image" content="https://formal.land/img/land-512.png"><meta data-react-helmet="true" property="og:url" content="https://formal.land/blog/2023/08/25/trait-representation-in-coq"><meta data-react-helmet="true" name="docusaurus_locale" content="en"><meta data-react-helmet="true" name="docusaurus_tag" content="default"><meta data-react-helmet="true" property="og:title" content="Trait representation in Coq | Formal Land"><meta data-react-helmet="true" name="description" content="In our project coq-of-rust we translate programs written in Rust to equivalent programs in the language of the proof system Coq&amp;nbsp;🐓, which will later allow us to formally verify them."><meta data-react-helmet="true" property="og:description" content="In our project coq-of-rust we translate programs written in Rust to equivalent programs in the language of the proof system Coq&amp;nbsp;🐓, which will later allow us to formally verify them."><meta data-react-helmet="true" property="og:type" content="article"><meta data-react-helmet="true" property="article:published_time" content="2023-08-25T00:00:00.000Z"><meta data-react-helmet="true" property="article:tag" content="coq-of-rust,Rust,Coq,trait"><link data-react-helmet="true" rel="icon" href="/img/land-512.png"><link data-react-helmet="true" rel="canonical" href="https://formal.land/blog/2023/08/25/trait-representation-in-coq"><link data-react-helmet="true" rel="alternate" href="https://formal.land/blog/2023/08/25/trait-representation-in-coq" hreflang="en"><link data-react-helmet="true" rel="alternate" href="https://formal.land/blog/2023/08/25/trait-representation-in-coq" hreflang="x-default"><link rel="stylesheet" href="/assets/css/styles.20dc303f.css">
 <link rel="preload" href="/assets/js/runtime~main.d15936f4.js" as="script">
-<link rel="preload" href="/assets/js/main.31e3dc13.js" as="script">
+<link rel="preload" href="/assets/js/main.5b0bc398.js" as="script">
 </head>
 <body>
 <script>!function(){function t(t){document.documentElement.setAttribute("data-theme",t)}var e=function(){var t=null;try{t=localStorage.getItem("theme")}catch(t){}return t}();t(null!==e?e:"light")}(),document.documentElement.setAttribute("data-announcement-bar-initially-dismissed",function(){try{return"true"===localStorage.getItem("docusaurus.announcement.dismiss")}catch(t){}return!1}())</script><div id="__docusaurus">
-<div><a href="#" class="skipToContent_1oUP">Skip to main content</a></div><div class="announcementBar_3WsW" style="background-color:#fafbfc;color:#091E42" role="banner"><div class="announcementBarContent_3EUC">For formal verification services, email us at <a href="mailto:&#099;&#111;&#110;&#116;&#097;&#099;&#116;&#064;formal&#046;&#108;&#097;&#110;&#100;">&#099;&#111;&#110;&#116;&#097;&#099;&#116;&#064;formal&#046;&#108;&#097;&#110;&#100;</a>! (Rust or OCaml)</div></div><nav class="navbar navbar--fixed-top"><div class="navbar__inner"><div class="navbar__items"><button aria-label="Navigation bar toggle" class="navbar__toggle clean-btn" type="button" tabindex="0"><svg width="30" height="30" viewBox="0 0 30 30" aria-hidden="true"><path stroke="currentColor" stroke-linecap="round" stroke-miterlimit="10" stroke-width="2" d="M4 7h22M4 15h22M4 23h22"></path></svg></button><a class="navbar__brand" href="/"><div class="navbar__logo"><img src="/img/land-512.png" alt="Logo" class="themedImage_1VuW themedImage--light_3UqQ"><img src="/img/land-512.png" alt="Logo" class="themedImage_1VuW themedImage--dark_hz6m"></div><b class="navbar__title">Formal Land</b></a><a class="navbar__item navbar__link" href="/docs/company/about">Company</a><a class="navbar__item navbar__link" href="/docs/verification/ocaml">Formal verification</a><a class="navbar__item navbar__link" href="/docs/services/solidity-development">Services</a><a class="navbar__item navbar__link" href="/docs/coq-of-ocaml/introduction">coq-of-ocaml</a><a aria-current="page" class="navbar__item navbar__link navbar__link--active" href="/blog">Blog</a></div><div class="navbar__items navbar__items--right"><a href="https://github.com/formal-land" target="_blank" rel="noopener noreferrer" class="navbar__item navbar__link"><span>GitHub<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_3J9K"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></span></a><a href="https://gitlab.com/formal-land" target="_blank" rel="noopener noreferrer" class="navbar__item navbar__link"><span>GitLab<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_3J9K"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></span></a></div></div><div role="presentation" class="navbar-sidebar__backdrop"></div></nav><div class="main-wrapper blog-wrapper blog-post-page"><div class="container margin-vert--lg"><div class="row"><aside class="col col--3"><nav class="sidebar_2ahu thin-scrollbar" aria-label="Blog recent posts navigation"><div class="sidebarItemTitle_2hhb margin-bottom--md">Recent posts</div><ul class="sidebarItemList_2xAf"><li class="sidebarItem_2UVv"><a class="sidebarItemLink_1RT6" href="/blog/2024/01/18/update-coq-of-rust">Upgrade the Rust version of coq-of-rust</a></li><li class="sidebarItem_2UVv"><a class="sidebarItemLink_1RT6" href="/blog/2024/01/04/rust-translating-match">Translating Rust match patterns to Coq with coq-of-rust</a></li><li class="sidebarItem_2UVv"><a class="sidebarItemLink_1RT6" href="/blog/2023/12/13/rust-verify-erc-20-smart-contract">Verifying an ERC-20 smart contract in Rust</a></li><li class="sidebarItem_2UVv"><a class="sidebarItemLink_1RT6" href="/blog/2023/11/26/rust-function-body">Translation of function bodies from Rust to Coq</a></li><li class="sidebarItem_2UVv"><a class="sidebarItemLink_1RT6" href="/blog/2023/11/08/rust-thir-and-bundled-traits">Optimizing Rust translation to Coq with THIR and bundled traits</a></li></ul></nav></aside><main class="col col--7" itemscope="" itemtype="http://schema.org/Blog"><article itemprop="blogPost" itemscope="" itemtype="http://schema.org/BlogPosting"><header><h1 class="blogPostTitle_GeHD" itemprop="headline">Trait representation in Coq</h1><div class="blogPostData_291c margin-vert--md"><time datetime="2023-08-25T00:00:00.000Z" itemprop="datePublished">August 25, 2023</time> · <!-- -->8 min read</div><div class="row margin-top--md margin-bottom--sm"><div class="col col--6 authorCol_1R69"><div class="avatar margin-bottom--sm"><div class="avatar__intro" itemprop="author" itemscope="" itemtype="https://schema.org/Person"><div class="avatar__name"><a itemprop="url"><span itemprop="name">Bartłomiej Królikowski</span></a></div></div></div></div></div></header><div class="markdown" itemprop="articleBody"><p>In our project <a href="https://github.com/formal-land/coq-of-rust" target="_blank" rel="noopener noreferrer">coq-of-rust</a> we translate programs written in <a href="https://www.rust-lang.org/" target="_blank" rel="noopener noreferrer">Rust</a> to equivalent programs in the language of the proof system <a href="https://coq.inria.fr/" target="_blank" rel="noopener noreferrer">Coq<!-- --> <!-- -->🐓</a>, which will later allow us to formally verify them.
+<div><a href="#" class="skipToContent_1oUP">Skip to main content</a></div><div class="announcementBar_3WsW" style="background-color:#fafbfc;color:#091E42" role="banner"><div class="announcementBarContent_3EUC">For formal verification services, email us at <a href="mailto:&#099;&#111;&#110;&#116;&#097;&#099;&#116;&#064;formal&#046;&#108;&#097;&#110;&#100;">&#099;&#111;&#110;&#116;&#097;&#099;&#116;&#064;formal&#046;&#108;&#097;&#110;&#100;</a>! (Rust, OCaml)</div></div><nav class="navbar navbar--fixed-top"><div class="navbar__inner"><div class="navbar__items"><button aria-label="Navigation bar toggle" class="navbar__toggle clean-btn" type="button" tabindex="0"><svg width="30" height="30" viewBox="0 0 30 30" aria-hidden="true"><path stroke="currentColor" stroke-linecap="round" stroke-miterlimit="10" stroke-width="2" d="M4 7h22M4 15h22M4 23h22"></path></svg></button><a class="navbar__brand" href="/"><div class="navbar__logo"><img src="/img/land-512.png" alt="Logo" class="themedImage_1VuW themedImage--light_3UqQ"><img src="/img/land-512.png" alt="Logo" class="themedImage_1VuW themedImage--dark_hz6m"></div><b class="navbar__title">Formal Land</b></a><a class="navbar__item navbar__link" href="/docs/company/about">Company</a><a class="navbar__item navbar__link" href="/docs/verification/ocaml">Formal verification</a><a class="navbar__item navbar__link" href="/docs/services/solidity-development">Services</a><a class="navbar__item navbar__link" href="/docs/coq-of-ocaml/introduction">coq-of-ocaml</a><a aria-current="page" class="navbar__item navbar__link navbar__link--active" href="/blog">Blog</a></div><div class="navbar__items navbar__items--right"><a href="https://github.com/formal-land" target="_blank" rel="noopener noreferrer" class="navbar__item navbar__link"><span>GitHub<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_3J9K"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></span></a><a href="https://gitlab.com/formal-land" target="_blank" rel="noopener noreferrer" class="navbar__item navbar__link"><span>GitLab<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_3J9K"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></span></a></div></div><div role="presentation" class="navbar-sidebar__backdrop"></div></nav><div class="main-wrapper blog-wrapper blog-post-page"><div class="container margin-vert--lg"><div class="row"><aside class="col col--3"><nav class="sidebar_2ahu thin-scrollbar" aria-label="Blog recent posts navigation"><div class="sidebarItemTitle_2hhb margin-bottom--md">Recent posts</div><ul class="sidebarItemList_2xAf"><li class="sidebarItem_2UVv"><a class="sidebarItemLink_1RT6" href="/blog/2024/01/18/update-coq-of-rust">Upgrade the Rust version of coq-of-rust</a></li><li class="sidebarItem_2UVv"><a class="sidebarItemLink_1RT6" href="/blog/2024/01/04/rust-translating-match">Translating Rust match patterns to Coq with coq-of-rust</a></li><li class="sidebarItem_2UVv"><a class="sidebarItemLink_1RT6" href="/blog/2023/12/13/rust-verify-erc-20-smart-contract">Verifying an ERC-20 smart contract in Rust</a></li><li class="sidebarItem_2UVv"><a class="sidebarItemLink_1RT6" href="/blog/2023/11/26/rust-function-body">Translation of function bodies from Rust to Coq</a></li><li class="sidebarItem_2UVv"><a class="sidebarItemLink_1RT6" href="/blog/2023/11/08/rust-thir-and-bundled-traits">Optimizing Rust translation to Coq with THIR and bundled traits</a></li></ul></nav></aside><main class="col col--7" itemscope="" itemtype="http://schema.org/Blog"><article itemprop="blogPost" itemscope="" itemtype="http://schema.org/BlogPosting"><header><h1 class="blogPostTitle_GeHD" itemprop="headline">Trait representation in Coq</h1><div class="blogPostData_291c margin-vert--md"><time datetime="2023-08-25T00:00:00.000Z" itemprop="datePublished">August 25, 2023</time> · <!-- -->8 min read</div><div class="row margin-top--md margin-bottom--sm"><div class="col col--6 authorCol_1R69"><div class="avatar margin-bottom--sm"><div class="avatar__intro" itemprop="author" itemscope="" itemtype="https://schema.org/Person"><div class="avatar__name"><a itemprop="url"><span itemprop="name">Bartłomiej Królikowski</span></a></div></div></div></div></div></header><div class="markdown" itemprop="articleBody"><p>In our project <a href="https://github.com/formal-land/coq-of-rust" target="_blank" rel="noopener noreferrer">coq-of-rust</a> we translate programs written in <a href="https://www.rust-lang.org/" target="_blank" rel="noopener noreferrer">Rust</a> to equivalent programs in the language of the proof system <a href="https://coq.inria.fr/" target="_blank" rel="noopener noreferrer">Coq<!-- --> <!-- -->🐓</a>, which will later allow us to formally verify them.
 Both Coq and Rust have many unique features, and there are many differences between them, so in the process of translation we need to treat the case of each language construction separately.
 In this post, we discuss how we translate the most complicated one: <a href="https://doc.rust-lang.org/book/ch10-02-traits.html" target="_blank" rel="noopener noreferrer">traits</a>.</p><h2 class="anchor anchorWithStickyNavbar_31ik" id="-traits-in-rust">🦀 Traits in Rust<a class="hash-link" href="#-traits-in-rust" title="Direct link to heading"></a></h2><p>Trait is the way to define a shared behaviour for a group of types in Rust.
 To define a trait we have to specify a list of signatures of the methods we want to be implemented for the types implementing our trait.
@@ -32,6 +32,6 @@
 <noscript><a href="https://www.livechat.com/chat-with/14938650/" rel="nofollow">Chat with us</a>, powered by <a href="https://www.livechat.com/?welcome" rel="noopener nofollow" target="_blank">LiveChat</a></noscript>
 <!-- End of LiveChat code --></div></div></div></footer></div>
 <script src="/assets/js/runtime~main.d15936f4.js"></script>
-<script src="/assets/js/main.31e3dc13.js"></script>
+<script src="/assets/js/main.5b0bc398.js"></script>
 </body>
 </html>
diff --git a/blog/2023/11/08/rust-thir-and-bundled-traits.html b/blog/2023/11/08/rust-thir-and-bundled-traits.html
diff --git a/blog/2023/11/26/rust-function-body.html b/blog/2023/11/26/rust-function-body.html
diff --git a/blog/2023/12/13/rust-verify-erc-20-smart-contract.html b/blog/2023/12/13/rust-verify-erc-20-smart-contract.html
diff --git a/blog/2024/01/04/rust-translating-match.html b/blog/2024/01/04/rust-translating-match.html
diff --git a/blog/2024/01/18/update-coq-of-rust.html b/blog/2024/01/18/update-coq-of-rust.html