diff --git a/archives/index.html b/archives/index.html
index 72d1908..9f610b9 100644
--- a/archives/index.html
+++ b/archives/index.html
@@ -1,6 +1,6 @@
 <!doctype html><html lang=en dir=auto><head><meta charset=utf-8><meta http-equiv=X-UA-Compatible content="IE=edge"><meta name=viewport content="width=device-width,initial-scale=1,shrink-to-fit=no"><meta name=robots content="index, follow"><title>Archive | hax</title>
 <meta name=keywords content><meta name=description content="archives"><meta name=author content="hacspec authors"><link rel=canonical href=https://hacspec.github.io/blog/archives/><link crossorigin=anonymous href=/blog/assets/css/stylesheet.1b82bbed8b13f853704558d527b681efaea938ce91e6ae8903e8b19e73b1b0f8.css integrity="sha256-G4K77YsT+FNwRVjVJ7aB766pOM6R5q6JA+ixnnOxsPg=" rel="preload stylesheet" as=style><link rel=icon href=https://hacspec.github.io/blog/favicon.ico><link rel=icon type=image/png sizes=16x16 href=https://hacspec.github.io/blog/favicon-16x16.png><link rel=icon type=image/png sizes=32x32 href=https://hacspec.github.io/blog/favicon-32x32.png><link rel=apple-touch-icon href=https://hacspec.github.io/blog/apple-touch-icon.png><link rel=mask-icon href=https://hacspec.github.io/blog/safari-pinned-tab.svg><meta name=theme-color content="#2e2e33"><meta name=msapplication-TileColor content="#2e2e33"><noscript><style>#theme-toggle,.top-link{display:none}</style><style>@media(prefers-color-scheme:dark){:root{--theme:rgb(29, 30, 32);--entry:rgb(46, 46, 51);--primary:rgb(218, 218, 219);--secondary:rgb(155, 156, 157);--tertiary:rgb(65, 66, 68);--content:rgb(196, 196, 197);--hljs-bg:rgb(46, 46, 51);--code-bg:rgb(55, 56, 62);--border:rgb(51, 51, 51)}.list{background:var(--theme)}.list:not(.dark)::-webkit-scrollbar-track{background:0 0}.list:not(.dark)::-webkit-scrollbar-thumb{border-color:var(--theme)}}</style></noscript><meta property="og:title" content="Archive"><meta property="og:description" content="archives"><meta property="og:type" content="article"><meta property="og:url" content="https://hacspec.github.io/blog/archives/"><meta property="og:image" content="https://hacspec.github.io/blog/papermod-cover.png"><meta property="article:section" content><meta name=twitter:card content="summary_large_image"><meta name=twitter:image content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:title content="Archive"><meta name=twitter:description content="archives"><script type=application/ld+json>{"@context":"https://schema.org","@type":"BreadcrumbList","itemListElement":[{"@type":"ListItem","position":1,"name":"Archive","item":"https://hacspec.github.io/blog/archives/"}]}</script><script type=application/ld+json>{"@context":"https://schema.org","@type":"BlogPosting","headline":"Archive","name":"Archive","description":"archives","keywords":[],"articleBody":"","wordCount":"0","inLanguage":"en","datePublished":"0001-01-01T00:00:00Z","dateModified":"0001-01-01T00:00:00Z","author":{"@type":"Person","name":"hacspec authors"},"mainEntityOfPage":{"@type":"WebPage","@id":"https://hacspec.github.io/blog/archives/"},"publisher":{"@type":"Organization","name":"hax","logo":{"@type":"ImageObject","url":"https://hacspec.github.io/blog/favicon.ico"}}}</script></head><body class=list id=top><script>localStorage.getItem("pref-theme")==="dark"?document.body.classList.add("dark"):localStorage.getItem("pref-theme")==="light"?document.body.classList.remove("dark"):window.matchMedia("(prefers-color-scheme: dark)").matches&&document.body.classList.add("dark")</script><header class=header><nav class=nav><div class=logo><a href=https://hacspec.github.io/blog/ accesskey=h title="hax (Alt + H)">hax</a><div class=logo-switches><button id=theme-toggle accesskey=t title="(Alt + T)"><svg id="moon" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M21 12.79A9 9 0 1111.21 3 7 7 0 0021 12.79z"/></svg><svg id="sun" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><circle cx="12" cy="12" r="5"/><line x1="12" y1="1" x2="12" y2="3"/><line x1="12" y1="21" x2="12" y2="23"/><line x1="4.22" y1="4.22" x2="5.64" y2="5.64"/><line x1="18.36" y1="18.36" x2="19.78" y2="19.78"/><line x1="1" y1="12" x2="3" y2="12"/><line x1="21" y1="12" x2="23" y2="12"/><line x1="4.22" y1="19.78" x2="5.64" y2="18.36"/><line x1="18.36" y1="5.64" x2="19.78" y2="4.22"/></svg></button></div></div><ul id=menu><li><a href=https://hacspec.github.io/blog/archives title=Archive><span class=active>Archive</span></a></li><li><a href=https://hacspec.github.io/blog/search/ title="Search (Alt + /)" accesskey=/><span>Search</span></a></li><li><a href=https://hacspec.github.io/blog/tags/ title=Tags><span>Tags</span></a></li></ul></nav></header><main class=main><header class=page-header><h1>Archive
-<a href=/blog/index.xml title=RSS aria-label=RSS><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" height="23"><path d="M4 11a9 9 0 019 9"/><path d="M4 4a16 16 0 0116 16"/><circle cx="5" cy="19" r="1"/></svg></a></h1></header><div class=archive-year><h2 class=archive-year-header>2024<sup class=archive-count>&nbsp;&nbsp;3</sup></h2><div class=archive-month><h3 class=archive-month-header>August<sup class=archive-count>&nbsp;&nbsp;1</sup></h3><div class=archive-posts><div class=archive-entry><h3 class=archive-entry-title>This month in hax: July 2024</h3><div class=archive-meta><span title='2024-08-12 00:00:00 +0000 UTC'>August 12, 2024</span>&nbsp;·&nbsp;2 min&nbsp;·&nbsp;Lucas Franceschino</div><a class=entry-link aria-label="post link to This month in hax: July 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-07/></a></div></div></div><div class=archive-month><h3 class=archive-month-header>July<sup class=archive-count>&nbsp;&nbsp;1</sup></h3><div class=archive-posts><div class=archive-entry><h3 class=archive-entry-title>This month in hax: June 2024</h3><div class=archive-meta><span title='2024-07-02 00:00:00 +0000 UTC'>July 2, 2024</span>&nbsp;·&nbsp;2 min&nbsp;·&nbsp;Lucas Franceschino</div><a class=entry-link aria-label="post link to This month in hax: June 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-06/></a></div></div></div><div class=archive-month><h3 class=archive-month-header>May<sup class=archive-count>&nbsp;&nbsp;1</sup></h3><div class=archive-posts><div class=archive-entry><h3 class=archive-entry-title>Announcing the hax tutorial</h3><div class=archive-meta><span title='2024-05-13 00:00:00 +0000 UTC'>May 13, 2024</span>&nbsp;·&nbsp;1 min&nbsp;·&nbsp;Lucas Franceschino</div><a class=entry-link aria-label="post link to Announcing the hax tutorial" href=https://hacspec.github.io/blog/posts/announcement-tutorial/></a></div></div></div></div><div class=archive-year><h2 class=archive-year-header>2023<sup class=archive-count>&nbsp;&nbsp;1</sup></h2><div class=archive-month><h3 class=archive-month-header>October<sup class=archive-count>&nbsp;&nbsp;1</sup></h3><div class=archive-posts><div class=archive-entry><h3 class=archive-entry-title>Introducing hax 🎂</h3><div class=archive-meta><span title='2023-10-20 00:00:00 +0000 UTC'>October 20, 2023</span>&nbsp;·&nbsp;7 min&nbsp;·&nbsp;Franziskus Kiefer & Lucas Franceschino</div><a class=entry-link aria-label="post link to Introducing hax 🎂" href=https://hacspec.github.io/blog/posts/hax-v0-1/></a></div></div></div></div></main><footer class=footer><span>&copy; 2024 <a href=https://hacspec.github.io/blog/>hax</a></span>
+<a href=/blog/index.xml title=RSS aria-label=RSS><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" height="23"><path d="M4 11a9 9 0 019 9"/><path d="M4 4a16 16 0 0116 16"/><circle cx="5" cy="19" r="1"/></svg></a></h1></header><div class=archive-year><h2 class=archive-year-header>2024<sup class=archive-count>&nbsp;&nbsp;4</sup></h2><div class=archive-month><h3 class=archive-month-header>October<sup class=archive-count>&nbsp;&nbsp;1</sup></h3><div class=archive-posts><div class=archive-entry><h3 class=archive-entry-title>This month in hax: September 2024</h3><div class=archive-meta><span title='2024-10-01 00:00:00 +0000 UTC'>October 1, 2024</span>&nbsp;·&nbsp;2 min&nbsp;·&nbsp;Lucas Franceschino</div><a class=entry-link aria-label="post link to This month in hax: September 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/></a></div></div></div><div class=archive-month><h3 class=archive-month-header>August<sup class=archive-count>&nbsp;&nbsp;1</sup></h3><div class=archive-posts><div class=archive-entry><h3 class=archive-entry-title>This month in hax: July 2024</h3><div class=archive-meta><span title='2024-08-12 00:00:00 +0000 UTC'>August 12, 2024</span>&nbsp;·&nbsp;2 min&nbsp;·&nbsp;Lucas Franceschino</div><a class=entry-link aria-label="post link to This month in hax: July 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-07/></a></div></div></div><div class=archive-month><h3 class=archive-month-header>July<sup class=archive-count>&nbsp;&nbsp;1</sup></h3><div class=archive-posts><div class=archive-entry><h3 class=archive-entry-title>This month in hax: June 2024</h3><div class=archive-meta><span title='2024-07-02 00:00:00 +0000 UTC'>July 2, 2024</span>&nbsp;·&nbsp;2 min&nbsp;·&nbsp;Lucas Franceschino</div><a class=entry-link aria-label="post link to This month in hax: June 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-06/></a></div></div></div><div class=archive-month><h3 class=archive-month-header>May<sup class=archive-count>&nbsp;&nbsp;1</sup></h3><div class=archive-posts><div class=archive-entry><h3 class=archive-entry-title>Announcing the hax tutorial</h3><div class=archive-meta><span title='2024-05-13 00:00:00 +0000 UTC'>May 13, 2024</span>&nbsp;·&nbsp;1 min&nbsp;·&nbsp;Lucas Franceschino</div><a class=entry-link aria-label="post link to Announcing the hax tutorial" href=https://hacspec.github.io/blog/posts/announcement-tutorial/></a></div></div></div></div><div class=archive-year><h2 class=archive-year-header>2023<sup class=archive-count>&nbsp;&nbsp;1</sup></h2><div class=archive-month><h3 class=archive-month-header>October<sup class=archive-count>&nbsp;&nbsp;1</sup></h3><div class=archive-posts><div class=archive-entry><h3 class=archive-entry-title>Introducing hax 🎂</h3><div class=archive-meta><span title='2023-10-20 00:00:00 +0000 UTC'>October 20, 2023</span>&nbsp;·&nbsp;7 min&nbsp;·&nbsp;Franziskus Kiefer & Lucas Franceschino</div><a class=entry-link aria-label="post link to Introducing hax 🎂" href=https://hacspec.github.io/blog/posts/hax-v0-1/></a></div></div></div></div></main><footer class=footer><span>&copy; 2024 <a href=https://hacspec.github.io/blog/>hax</a></span>
 <span>Powered by
 <a href=https://gohugo.io/ rel="noopener noreferrer" target=_blank>Hugo</a> &
         <a href=https://github.com/adityatelange/hugo-PaperMod/ rel=noopener target=_blank>PaperMod</a></span></footer><a href=#top aria-label="go to top" title="Go to Top (Alt + G)" class=top-link id=top-link accesskey=g><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 12 6" fill="currentcolor"><path d="M12 6H0l6-6z"/></svg></a><script>let menu=document.getElementById("menu");menu&&(menu.scrollLeft=localStorage.getItem("menu-scroll-position"),menu.onscroll=function(){localStorage.setItem("menu-scroll-position",menu.scrollLeft)}),document.querySelectorAll('a[href^="#"]').forEach(e=>{e.addEventListener("click",function(e){e.preventDefault();var t=this.getAttribute("href").substr(1);window.matchMedia("(prefers-reduced-motion: reduce)").matches?document.querySelector(`[id='${decodeURIComponent(t)}']`).scrollIntoView():document.querySelector(`[id='${decodeURIComponent(t)}']`).scrollIntoView({behavior:"smooth"}),t==="top"?history.replaceState(null,null," "):history.pushState(null,null,`#${t}`)})})</script><script>var mybutton=document.getElementById("top-link");window.onscroll=function(){document.body.scrollTop>800||document.documentElement.scrollTop>800?(mybutton.style.visibility="visible",mybutton.style.opacity="1"):(mybutton.style.visibility="hidden",mybutton.style.opacity="0")}</script><script>document.getElementById("theme-toggle").addEventListener("click",()=>{document.body.className.includes("dark")?(document.body.classList.remove("dark"),localStorage.setItem("pref-theme","light")):(document.body.classList.add("dark"),localStorage.setItem("pref-theme","dark"))})</script></body></html>
\ No newline at end of file
diff --git a/index.html b/index.html
index 2bf1c51..4943ae8 100644
--- a/index.html
+++ b/index.html
@@ -1,5 +1,7 @@
 <!doctype html><html lang=en dir=auto><head><meta name=generator content="Hugo 0.121.0"><meta charset=utf-8><meta http-equiv=X-UA-Compatible content="IE=edge"><meta name=viewport content="width=device-width,initial-scale=1,shrink-to-fit=no"><meta name=robots content="index, follow"><title>hax</title>
-<meta name=description content="hax & hacspec blog - https://github.com/hacspec/blog"><meta name=author content="hacspec authors"><link rel=canonical href=https://hacspec.github.io/blog/><link crossorigin=anonymous href=/blog/assets/css/stylesheet.1b82bbed8b13f853704558d527b681efaea938ce91e6ae8903e8b19e73b1b0f8.css integrity="sha256-G4K77YsT+FNwRVjVJ7aB766pOM6R5q6JA+ixnnOxsPg=" rel="preload stylesheet" as=style><link rel=icon href=https://hacspec.github.io/blog/favicon.ico><link rel=icon type=image/png sizes=16x16 href=https://hacspec.github.io/blog/favicon-16x16.png><link rel=icon type=image/png sizes=32x32 href=https://hacspec.github.io/blog/favicon-32x32.png><link rel=apple-touch-icon href=https://hacspec.github.io/blog/apple-touch-icon.png><link rel=mask-icon href=https://hacspec.github.io/blog/safari-pinned-tab.svg><meta name=theme-color content="#2e2e33"><meta name=msapplication-TileColor content="#2e2e33"><link rel=alternate type=application/rss+xml href=https://hacspec.github.io/blog/index.xml><link rel=alternate type=application/json href=https://hacspec.github.io/blog/index.json><noscript><style>#theme-toggle,.top-link{display:none}</style><style>@media(prefers-color-scheme:dark){:root{--theme:rgb(29, 30, 32);--entry:rgb(46, 46, 51);--primary:rgb(218, 218, 219);--secondary:rgb(155, 156, 157);--tertiary:rgb(65, 66, 68);--content:rgb(196, 196, 197);--hljs-bg:rgb(46, 46, 51);--code-bg:rgb(55, 56, 62);--border:rgb(51, 51, 51)}.list{background:var(--theme)}.list:not(.dark)::-webkit-scrollbar-track{background:0 0}.list:not(.dark)::-webkit-scrollbar-thumb{border-color:var(--theme)}}</style></noscript><meta property="og:title" content="hax"><meta property="og:description" content="hax & hacspec blog - https://github.com/hacspec/blog"><meta property="og:type" content="website"><meta property="og:url" content="https://hacspec.github.io/blog/"><meta property="og:image" content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:card content="summary_large_image"><meta name=twitter:image content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:title content="hax"><meta name=twitter:description content="hax & hacspec blog - https://github.com/hacspec/blog"><script type=application/ld+json>{"@context":"https://schema.org","@type":"Organization","name":"hax","url":"https://hacspec.github.io/blog/","description":"hax \u0026amp; hacspec blog - https://github.com/hacspec/blog","thumbnailUrl":"https://hacspec.github.io/blog/favicon.ico","sameAs":["https://github.com/hacspec/hax","mailto:hacspec@cryspen.com"]}</script></head><body class=list id=top><script>localStorage.getItem("pref-theme")==="dark"?document.body.classList.add("dark"):localStorage.getItem("pref-theme")==="light"?document.body.classList.remove("dark"):window.matchMedia("(prefers-color-scheme: dark)").matches&&document.body.classList.add("dark")</script><header class=header><nav class=nav><div class=logo><a href=https://hacspec.github.io/blog/ accesskey=h title="hax (Alt + H)">hax</a><div class=logo-switches><button id=theme-toggle accesskey=t title="(Alt + T)"><svg id="moon" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M21 12.79A9 9 0 1111.21 3 7 7 0 0021 12.79z"/></svg><svg id="sun" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><circle cx="12" cy="12" r="5"/><line x1="12" y1="1" x2="12" y2="3"/><line x1="12" y1="21" x2="12" y2="23"/><line x1="4.22" y1="4.22" x2="5.64" y2="5.64"/><line x1="18.36" y1="18.36" x2="19.78" y2="19.78"/><line x1="1" y1="12" x2="3" y2="12"/><line x1="21" y1="12" x2="23" y2="12"/><line x1="4.22" y1="19.78" x2="5.64" y2="18.36"/><line x1="18.36" y1="5.64" x2="19.78" y2="4.22"/></svg></button></div></div><ul id=menu><li><a href=https://hacspec.github.io/blog/archives title=Archive><span>Archive</span></a></li><li><a href=https://hacspec.github.io/blog/search/ title="Search (Alt + /)" accesskey=/><span>Search</span></a></li><li><a href=https://hacspec.github.io/blog/tags/ title=Tags><span>Tags</span></a></li></ul></nav></header><main class=main><article class="first-entry home-info"><header class=entry-header><h1>hax & hacspec</h1></header><div class=entry-content>A Rust verification tool</div><footer class=entry-footer><div class=social-icons><a href=https://github.com/hacspec/hax target=_blank rel="noopener noreferrer me" title=Github><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M9 19c-5 1.5-5-2.5-7-3m14 6v-3.87a3.37 3.37.0 00-.94-2.61c3.14-.35 6.44-1.54 6.44-7A5.44 5.44.0 0020 4.77 5.07 5.07.0 0019.91 1S18.73.65 16 2.48a13.38 13.38.0 00-7 0C6.27.65 5.09 1 5.09 1A5.07 5.07.0 005 4.77 5.44 5.44.0 003.5 8.55c0 5.42 3.3 6.61 6.44 7A3.37 3.37.0 009 18.13V22"/></svg></a><a href=mailto:hacspec@cryspen.com target=_blank rel="noopener noreferrer me" title=Email><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 21" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M4 4h16c1.1.0 2 .9 2 2v12c0 1.1-.9 2-2 2H4c-1.1.0-2-.9-2-2V6c0-1.1.9-2 2-2z"/><polyline points="22,6 12,13 2,6"/></svg></a></div></footer></article><article class=post-entry><header class=entry-header><h2>This month in hax: July 2024</h2></header><div class=entry-content><p>In July, we merged 32 PRs! 🎉
+<meta name=description content="hax & hacspec blog - https://github.com/hacspec/blog"><meta name=author content="hacspec authors"><link rel=canonical href=https://hacspec.github.io/blog/><link crossorigin=anonymous href=/blog/assets/css/stylesheet.1b82bbed8b13f853704558d527b681efaea938ce91e6ae8903e8b19e73b1b0f8.css integrity="sha256-G4K77YsT+FNwRVjVJ7aB766pOM6R5q6JA+ixnnOxsPg=" rel="preload stylesheet" as=style><link rel=icon href=https://hacspec.github.io/blog/favicon.ico><link rel=icon type=image/png sizes=16x16 href=https://hacspec.github.io/blog/favicon-16x16.png><link rel=icon type=image/png sizes=32x32 href=https://hacspec.github.io/blog/favicon-32x32.png><link rel=apple-touch-icon href=https://hacspec.github.io/blog/apple-touch-icon.png><link rel=mask-icon href=https://hacspec.github.io/blog/safari-pinned-tab.svg><meta name=theme-color content="#2e2e33"><meta name=msapplication-TileColor content="#2e2e33"><link rel=alternate type=application/rss+xml href=https://hacspec.github.io/blog/index.xml><link rel=alternate type=application/json href=https://hacspec.github.io/blog/index.json><noscript><style>#theme-toggle,.top-link{display:none}</style><style>@media(prefers-color-scheme:dark){:root{--theme:rgb(29, 30, 32);--entry:rgb(46, 46, 51);--primary:rgb(218, 218, 219);--secondary:rgb(155, 156, 157);--tertiary:rgb(65, 66, 68);--content:rgb(196, 196, 197);--hljs-bg:rgb(46, 46, 51);--code-bg:rgb(55, 56, 62);--border:rgb(51, 51, 51)}.list{background:var(--theme)}.list:not(.dark)::-webkit-scrollbar-track{background:0 0}.list:not(.dark)::-webkit-scrollbar-thumb{border-color:var(--theme)}}</style></noscript><meta property="og:title" content="hax"><meta property="og:description" content="hax & hacspec blog - https://github.com/hacspec/blog"><meta property="og:type" content="website"><meta property="og:url" content="https://hacspec.github.io/blog/"><meta property="og:image" content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:card content="summary_large_image"><meta name=twitter:image content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:title content="hax"><meta name=twitter:description content="hax & hacspec blog - https://github.com/hacspec/blog"><script type=application/ld+json>{"@context":"https://schema.org","@type":"Organization","name":"hax","url":"https://hacspec.github.io/blog/","description":"hax \u0026amp; hacspec blog - https://github.com/hacspec/blog","thumbnailUrl":"https://hacspec.github.io/blog/favicon.ico","sameAs":["https://github.com/hacspec/hax","mailto:hacspec@cryspen.com"]}</script></head><body class=list id=top><script>localStorage.getItem("pref-theme")==="dark"?document.body.classList.add("dark"):localStorage.getItem("pref-theme")==="light"?document.body.classList.remove("dark"):window.matchMedia("(prefers-color-scheme: dark)").matches&&document.body.classList.add("dark")</script><header class=header><nav class=nav><div class=logo><a href=https://hacspec.github.io/blog/ accesskey=h title="hax (Alt + H)">hax</a><div class=logo-switches><button id=theme-toggle accesskey=t title="(Alt + T)"><svg id="moon" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M21 12.79A9 9 0 1111.21 3 7 7 0 0021 12.79z"/></svg><svg id="sun" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><circle cx="12" cy="12" r="5"/><line x1="12" y1="1" x2="12" y2="3"/><line x1="12" y1="21" x2="12" y2="23"/><line x1="4.22" y1="4.22" x2="5.64" y2="5.64"/><line x1="18.36" y1="18.36" x2="19.78" y2="19.78"/><line x1="1" y1="12" x2="3" y2="12"/><line x1="21" y1="12" x2="23" y2="12"/><line x1="4.22" y1="19.78" x2="5.64" y2="18.36"/><line x1="18.36" y1="5.64" x2="19.78" y2="4.22"/></svg></button></div></div><ul id=menu><li><a href=https://hacspec.github.io/blog/archives title=Archive><span>Archive</span></a></li><li><a href=https://hacspec.github.io/blog/search/ title="Search (Alt + /)" accesskey=/><span>Search</span></a></li><li><a href=https://hacspec.github.io/blog/tags/ title=Tags><span>Tags</span></a></li></ul></nav></header><main class=main><article class="first-entry home-info"><header class=entry-header><h1>hax & hacspec</h1></header><div class=entry-content>A Rust verification tool</div><footer class=entry-footer><div class=social-icons><a href=https://github.com/hacspec/hax target=_blank rel="noopener noreferrer me" title=Github><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M9 19c-5 1.5-5-2.5-7-3m14 6v-3.87a3.37 3.37.0 00-.94-2.61c3.14-.35 6.44-1.54 6.44-7A5.44 5.44.0 0020 4.77 5.07 5.07.0 0019.91 1S18.73.65 16 2.48a13.38 13.38.0 00-7 0C6.27.65 5.09 1 5.09 1A5.07 5.07.0 005 4.77 5.44 5.44.0 003.5 8.55c0 5.42 3.3 6.61 6.44 7A3.37 3.37.0 009 18.13V22"/></svg></a><a href=mailto:hacspec@cryspen.com target=_blank rel="noopener noreferrer me" title=Email><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 21" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M4 4h16c1.1.0 2 .9 2 2v12c0 1.1-.9 2-2 2H4c-1.1.0-2-.9-2-2V6c0-1.1.9-2 2-2z"/><polyline points="22,6 12,13 2,6"/></svg></a></div></footer></article><article class=post-entry><header class=entry-header><h2>This month in hax: September 2024</h2></header><div class=entry-content><p>In July, we merged 33 PRs! 🎉
+On the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. 'a in for&lt;'a> &'a T: PartialEq&lt;i32>) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code.
+In the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue....</p></div><footer class=entry-footer><span title='2024-10-01 00:00:00 +0000 UTC'>October 1, 2024</span>&nbsp;·&nbsp;2 min&nbsp;·&nbsp;Lucas Franceschino</footer><a class=entry-link aria-label="post link to This month in hax: September 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/></a></article><article class=post-entry><header class=entry-header><h2>This month in hax: July 2024</h2></header><div class=entry-content><p>In July, we merged 32 PRs! 🎉
 On the side of the frontend and CLI, we had a lot of fixes and improvements! The hax command line and rustc driver were refactored, allowing for better scaling and caching. We also improved the general ergonomics: diagnostics can now be output in JSON, we have improved error messages… And we pushed various bug fixes.
 In the engine, we now resugar asserts properly and support dyn....</p></div><footer class=entry-footer><span title='2024-08-12 00:00:00 +0000 UTC'>August 12, 2024</span>&nbsp;·&nbsp;2 min&nbsp;·&nbsp;Lucas Franceschino</footer><a class=entry-link aria-label="post link to This month in hax: July 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-07/></a></article><article class=post-entry><header class=entry-header><h2>This month in hax: June 2024</h2></header><div class=entry-content><p>This first blog post inaugurates our series named “This Month in hax”: a series of short highlights of what happened in the development of hax and it’s ecosystem in the month.
 In June, 23 PRs have been merged 🎉! The detail is available below.
diff --git a/index.json b/index.json
index f267aee..edcab0f 100644
--- a/index.json
+++ b/index.json
@@ -1 +1 @@
-[{"content":"In July, we merged 32 PRs! 🎉\nOn the side of the frontend and CLI, we had a lot of fixes and improvements! The hax command line and rustc driver were refactored, allowing for better scaling and caching. We also improved the general ergonomics: diagnostics can now be output in JSON, we have improved error messages\u0026hellip; And we pushed various bug fixes.\nIn the engine, we now resugar asserts properly and support dyn. We also pushed various enhancements (visitors for the internal AST are generated again, we propagate some more trait generics arguments\u0026hellip;) and bug fixes.\nOn the topic of libraries and helper macros, users can now add requires and ensures clauses directly on traits.\nMerged Pull Requests #811: Add mli for phase_reconstruct_for_index_loops. #802: Add json format option #800: feat(engine/ocaml_of_json_schema): add val to keyword list #799: fix(bounded-ints): zero and one were inverted #797: Fix potentially looping predicate_id. #796: Add nicer error messages when rustc emits an error in detect_forking. #795: fix: precondition constraints should be of the shape true =\u0026gt; pred #794: Resugar asserts #792: feat(frontend): Add option to control output directory #790: Allow ensures and requires on traits #788: Fix #296 #779: Support let-else pattern. #777: Small typo fixes for hax book #776: feat(book): fix checkboxes #769: Extensions to the proof-libs for libcrux-ml-kem #765: fix(engine/lib): import associated item projection on generic bounds #764: feat(hax-lib): allow requires \u0026amp; ensures on \u0026amp;mut inputs functions #763: fix(hax-lib): refinements: various fixes #762: fix(hax-lib): use super::* in refinement expansion #759: fix(frontend): crashes on fn ptr #758: fix color printing in util script #756: fix(frontend): kill crate_type in HaxMeta #753: exporter: make it need nightly only when feature rustc is on #751: Engine: propagate trait generics arguments #750: feat(exporter): thir: call: separate trait VS method generic args #744: doc(engine): ppx_functor_application #743: Refactor of the frontend #730: fix(frontend): make path_to breadth-first #729: Move book from hacspec/book to hacspec/hax #727: fix(engine): Concrete_ident_generated: name -\u0026gt; t, derive more #698: Generate visitors automatically Contributors paulmure maximebuyse karthikbhargavan W95Psp ","permalink":"https://hacspec.github.io/blog/posts/this-month-in-hax/2024-07/","summary":"In July, we merged 32 PRs! 🎉\nOn the side of the frontend and CLI, we had a lot of fixes and improvements! The hax command line and rustc driver were refactored, allowing for better scaling and caching. We also improved the general ergonomics: diagnostics can now be output in JSON, we have improved error messages\u0026hellip; And we pushed various bug fixes.\nIn the engine, we now resugar asserts properly and support dyn.","title":"This month in hax: July 2024"},{"content":"This first blog post inaugurates our series named \u0026ldquo;This Month in hax\u0026rdquo;: a series of short highlights of what happened in the development of hax and it\u0026rsquo;s ecosystem in the month.\nIn June, 23 PRs have been merged 🎉! The detail is available below.\nOn the Rust side, we have updated the Rust compiler to a very recent nightly thanks to @Nadrieril! We also added support for more Rust features in the frontend (dyn Trait), more disciminant informations on ADTs, fixed various bugs, and improved the general experience of using hax.\nWe pushed many fixes for the F* backend in the engine and improved the F* proof library. We also improved the bounded integer library and it\u0026rsquo;s F* integration.\nMerged Pull Requests Translate dyn Trait information fix(engine/fstar): use Base.String.hash instead of String.hash feat: add LICENSE Update rustc all at once refactor(engine/fstar-ast): get rid of zarith and GMP Update rustc fix(engine/fstar): fix implicit discrepancies in traits feat(nix): reduce closure size for hax-engine Generalize bounded ints Don\u0026rsquo;t use strings to represent paths Update rustc fix(backends/fstar): no __marker_trait if parent bounds feat(proof-libs): add t_Default feat(hax): logging: enable tracing in release, add trait-related logs fix(exporter): disable impl expr resolution under type aliases fix: rename action for extracting ml-kem feat: isolate DefId: faster build times fix(README): always begin relative path with ./, rewrite in action fix(ci): newer version of ppx_deriving (6.0.2) loops indefinitely Update to OCaml 5 Export discriminant values in AdtDef Update README.md Bump rustc version ","permalink":"https://hacspec.github.io/blog/posts/this-month-in-hax/2024-06/","summary":"This first blog post inaugurates our series named \u0026ldquo;This Month in hax\u0026rdquo;: a series of short highlights of what happened in the development of hax and it\u0026rsquo;s ecosystem in the month.\nIn June, 23 PRs have been merged 🎉! The detail is available below.\nOn the Rust side, we have updated the Rust compiler to a very recent nightly thanks to @Nadrieril! We also added support for more Rust features in the frontend (dyn Trait), more disciminant informations on ADTs, fixed various bugs, and improved the general experience of using hax.","title":"This month in hax: June 2024"},{"content":"We have been applying hax to verify several Rust pieces of software recently. hax was used to verify Libcrux\u0026rsquo;s implementation of ML-KEM with F*, but also for smart contracts verification with Coq, and even on protocols with F* and our new ProVerif backend.\nMeanwhile, we also presented hax at several conferences and workshops. The need for more documentation and guidance was becoming apparent: it was about time to have a tutorial!\nNew resources to learn more about hax The hax book has three new chapters:\nThe Quick start chapter explains how to go from a simple Rust crate to an F* extraction via hax, including how to install the tooling. The Tutorial chapter goes more in-depth into using hax and F* together to prove various properties of Rust code. The FAQ chapter is a work in progress but is intended to answer pragmatically and with examples to precise common issues or questions. Feel free to open an issue on the book repository if you feel like a topic should be addressed! We also added several examples of Rust verification via hax and F* in the example directory of hax, please check them out!\n","permalink":"https://hacspec.github.io/blog/posts/announcement-tutorial/","summary":"We have been applying hax to verify several Rust pieces of software recently. hax was used to verify Libcrux\u0026rsquo;s implementation of ML-KEM with F*, but also for smart contracts verification with Coq, and even on protocols with F* and our new ProVerif backend.\nMeanwhile, we also presented hax at several conferences and workshops. The need for more documentation and guidance was becoming apparent: it was about time to have a tutorial!","title":"Announcing the hax tutorial"},{"content":"This has been in the making for a while now. But we are finally happy to announce the first release of hax. It is still early days and we only tagged v0.1. But a ton of work has gone into this release.\nWait, what is hax?\nLet\u0026rsquo;s start at the beginning. A group of us started hacspec (high assurance crypto specifications), a language for specifying cryptographic primitives as the basis for formal verification, in early 2018 at the HACS workshop. After two iterations on hacspec the project outgrew the name and the initial crypto-oriented scope.\nHere comes hax. hax is a tool for high assurance translations that translates a large-ish subset of safe Rust into the formal languages accepted by proof assistants such as F* or Coq. Backends for other provers like EasyCrypt are under construction.\nThis is the result of joint work between the Prosecco team at Inria, Cryspen, and Prof. Spitters\u0026rsquo; group at Aarhus University.\nThe key design principle behind hax is hat we want to build a usable tool for verifying Rust programs without forcing the user to commit to a specific proof environment. In the future, we hope multiple tool developers will find it fruitful to build backends for hax.\nSo what is hacspec now?\nhacspec is a purely functional subset of Rust that can be used, together with a hacspec standard library, to write succinct, executable, and verifiable specifications in Rust. These specifications can be translated into formal languages with hax.\nhax There are a number of Rust verification projects out there. See, for example, Rust Verify and the Rust Formal Methods Interest Group. While most existing tools try to precisely model the most complex bits the Rust language, hax aims to be a usable and pragmatic tool that can analyze the kind of code Rust developers write on a daily basis, while abstracting away or ignoring Rust features it does not support. We believe that it is important in practice to have a usable tool that can ingest large Rust crates to show properties on certain parts of the code, instead of getting stuck on hard corner cases.\nhax has two parts: the exporter and the engine.\nThe Exporter When hax is invoked on a Rust crate, the exporter hooks into the Rust compiler. Compiling a program, Rust transformes the user source code to various internal representations in an optimized fashion (essentially HIR, THIR and MIR, illustrated in the diagram below). While this is great within the compiler, those representations are not friendly to external tool consumption.\nThe hax exporter is a Rust driver that provides a bridge from those unstable internal representations to fixed and easy-to-consume ASTs1 (abstract syntax trees). The JSON node on the diagram below represents those ASTs.\nThe hax exporter is not opinionated toward the hax project: it can be used as a frontend to the Rust compiler in other projects. For example, we are working with the Aeneas project towards sharing the exporter code between the two tools.\nThe Engine The magic of hax really happens in the engine, written in OCaml. It directly consumes2 the output of the exporter, that is, the ASTs exported for your crate of choice.\nUpon the backend choice (for instance: shall we extract to F* or to Coq?), the engine proceeds to a sequence of typed3 program transformations, eventually landing into the sublanguage supported by the targeted language, e.g. F*.\nThe various program transformations are called phases. We have a dozen of them:\ntransforming and functionalizing for loops; functionalizing local mutation; rewrite functions with mutable references as inputs into state-passing code; and many more! Those phases are statically typed: for instance, making for loops functional is not possible on an AST that still contains local mutation. Such constraints are ensured statically, reducing opportunities for bugs.\nThis typed phase design allows us to target heterogeneous languages: for instance, we already support a backend in the imperative language of the SSProve Coq library. This comes with an automatic proof that it is equivalent to the functional interpretation. This can be seen as a case-by-case correctness proof of hax.\nThis design can be used as a template for the upcoming backend which targets the imperative language of EasyCrypt.\nUsage hax is still heavily under development. It is therefore recommended to install it straight from the git repository (see the Installation section in the readme).\nAfter installing it you can call it from any Rust crate.\ncargo hax into fstar This will extract the crate to F*. Similarly, cargo hax into coq will extract the crate to Coq.\nFor more options use\ncargo hax into --help Example We walk through a sample usage of hax based on an example. The example can be found in the git repository.\nGo to the proofs/fstar/extraction directory and run make. This will first call\ncargo hax into -i \u0026#39;-** +**::process_order\u0026#39; fstar in order to extract the process_order order function to F*. This demonstrates one particularly useful feature in hax, which allows extracting only a small portion or single function from a much larger crate. The argument -i '-** +**::process_order' tells hax to include the process_order function in any module and exclude (-**) everything else. In addition to the function itself, hax extracts all the required dependencies within the crate as well.\nRust fn process_order\u0026lt;T\u0026gt;(mut order: Order, other_side: \u0026amp;mut BinaryHeap\u0026lt;T\u0026gt;) -\u0026gt; (Vec\u0026lt;Match\u0026gt;, Option\u0026lt;Order\u0026gt;) where T: Into\u0026lt;Order\u0026gt; + From\u0026lt;Order\u0026gt; + Ord + Clone, { ... if let Some(m) = other_side .peek() .and_then(|other| Into::into(other.clone()).try_match(\u0026amp;order)) { order.quantity -= m.quantity; let mut other: Order = Into::into(other_side.pop().unwrap()); other.quantity -= m.quantity; if other.quantity \u0026gt; 0 { other_side.push(From::from(other.clone())); } matches.push(m); } else { done = true; } ... } F* match Core.Option.impl__and_then (Alloc.Collections.Binary_heap.impl_10__peek other_side \u0026lt;: Core.Option.t_Option v_T) (fun other -\u0026gt; impl__Order__try_match (Core.Convert.f_into (Core.Clone.f_clone other \u0026lt;: v_T) \u0026lt;: t_Order) order \u0026lt;: Core.Option.t_Option t_Match) \u0026lt;: Core.Option.t_Option t_Match with | Core.Option.Option_Some m -\u0026gt; let order:t_Order = { order with f_quantity = order.f_quantity -! m.f_quantity } in let tmp0, out:(Alloc.Collections.Binary_heap.t_BinaryHeap v_T \u0026amp; Core.Option.t_Option v_T) = Alloc.Collections.Binary_heap.impl_9__pop other_side in let other_side:Alloc.Collections.Binary_heap.t_BinaryHeap v_T = tmp0 in let hoist1:Core.Option.t_Option v_T = out in let hoist2:v_T = Core.Option.impl__unwrap hoist1 in let (other: t_Order):t_Order = Core.Convert.f_into hoist2 in let other:t_Order = { other with f_quantity = other.f_quantity -! m.f_quantity } in let other_side:Alloc.Collections.Binary_heap.t_BinaryHeap v_T = if other.f_quantity \u0026gt;. 0uL then let other_side:Alloc.Collections.Binary_heap.t_BinaryHeap v_T = Alloc.Collections.Binary_heap.impl_9__push other_side (Core.Convert.f_from (Core.Clone.f_clone other \u0026lt;: t_Order) \u0026lt;: v_T) in other_side else other_side in let matches:Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global = Alloc.Vec.impl_1__push matches m in done, matches, order, other_side | _ -\u0026gt; let done:bool = true in done, matches, order, other_side Then the makefile calls F* on the generated output. The successful typechecking in F* proves two properties on the Rust code.\nNon-panicking subtraction First, it shows that the lines with\norder.quantity -= m.quantity; do not underflow.\nConcretely, in Rust, the subtraction on u64 integers is a partial operation: the subtraction of x and y (x - y) is defined only when x is greater or equal to y such that x - y \u0026gt;= 0.\nSuch a requirement cannot be expressed as a Rust type, thus Rust\u0026rsquo;s subtraction panics (in debug mode) when it is called with bad inputs.\nIn contrast, F* is ideal to express such types! We model Rust\u0026rsquo;s subtraction as a total function with a strong type signature:\nval ( -! ): x: u64 -\u0026gt; y: u64 {x \u0026gt;=. y} -\u0026gt; u64 This strong signature implies a proof obligation: whenever this F* subtraction is used, F* won\u0026rsquo;t typecheck unless it finds a proof that x \u0026gt;=. y holds.\nTherefore, typechecking in F* implies that order.quantity -= m.quantity; never underflows.\nNon-panicking unwrap Second, it shows that\nother_side.pop().unwrap() never panics, i.e. the pop always returns Some value and thus unwrap never panics.\nSimilarly to subtraction, in F*, using unwrap requires a proof that the option being unwrapped is not None.\nCall to Action hax is still under heavy development and there are many features we want to add, and many bugs to squash. We invite everyone to contribute to the project with new backends, contributing to the hax frontend or backend, or provide examples to exercise the tool.\nThe F* backend is currently being developed by the Inria Prosecco team, the Coq backend by the Aarhus team, and an EasyCrypt backend is in the works by the EasyCrypt team. We are also working with the Aeneas project to allow better interoperability between their sophisticated stateful Rust verification toolchain and hax.\nResources Zulip Git Repository Rust\u0026rsquo;s internal ASTs are very optimized in memory and require constantly to lookup things interactively with the Rust compiler. Instead, our ASTs are indirection-free trees packing as much informations as possible (e.g. types, attributes, spans\u0026hellip;), ready for direct consumption.\u0026#160;\u0026#x21a9;\u0026#xfe0e;\nThe exporter expose big ASTs as JSON. The Rust type definitions of those ASTs are automatically converted into OCaml type definition along with JSON serializer and deserializers, using JSON Schemas.\u0026#160;\u0026#x21a9;\u0026#xfe0e;\nThe internal AST used by the hax engine is functorized. This enables AST transformations to be strongly typed.\u0026#160;\u0026#x21a9;\u0026#xfe0e;\n","permalink":"https://hacspec.github.io/blog/posts/hax-v0-1/","summary":"This has been in the making for a while now. But we are finally happy to announce the first release of hax. It is still early days and we only tagged v0.1. But a ton of work has gone into this release.\nWait, what is hax?\nLet\u0026rsquo;s start at the beginning. A group of us started hacspec (high assurance crypto specifications), a language for specifying cryptographic primitives as the basis for formal verification, in early 2018 at the HACS workshop.","title":"Introducing hax 🎂"}]
\ No newline at end of file
+[{"content":"In July, we merged 33 PRs! 🎉\nOn the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. 'a in for\u0026lt;'a\u0026gt; \u0026amp;'a T: PartialEq\u0026lt;i32\u0026gt;) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code.\nIn the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue.\nWe\u0026rsquo;ve been improving F* support and F* libraries. Importantly, cmester0 is working on a model of core, in Rust: we aim at replacing our hand-crafted F* model of core by an hax extraction of this new core model implemented in Rust. We will also be able to extract this model of core in every of our backends, enabling a uniform and pain-free core multi-backend library.\nMerged Pull Requests #934: chore: assign an issue id for every error in the engine #932: chore: assign an issue for every error in import_thir #919: fix #422 #918: chore: remove stale Hax.Lib.fst #917: doc: disambiguate_local_idents #916: update Cargo.lock #909: Revert \u0026ldquo;fix(engine/fstar): fix super typeclasses attributes\u0026rdquo; #908: fix(engine/deps): stop re-computing over and over the set of assoc items #907: Add RewriteControlFlow phase. #906: Cleanup trait resolution #902: fix(engine/fstar): fix super typeclasses attributes #901: Determine emuerate value by index #898: Fix some binder-related crashes #895: Don\u0026rsquo;t eval constants eagerly #894: Detangle trait solving from SInto #892: Support other variants of MIR #891: fix: fstar: default trait #887: Initial cleanup of binders-related code #885: docs(book): depend on hax-lib only when using hax #884: Fix incorrect line numbers in error messages #883: Fix step boundaries in fold_range_step_by #882: fix(fstar-core): add support for Option::map #880: Support float literals #877: Avoid recursing twice on the arguments. #876: Translate additional unsafe MIR operations #873: Small PR to fix circularity in Core.Fmt.fsti #872: Pre post impl blocks #870: count-ones post-condition #868: engine: kill a few exn to get useful errors #867: Backend: Import unsafe code as a gated feature #860: fix(engine): make dep. analysis sensible to UID assoc. items #827: Add infos impl #819: Add Rust Core Fstar Definitions. Contributors Nadrieril R1kM ROMemories W95Psp franziskuskiefer gaetan-sbt karthikbhargavan mamonet maximebuyse paulmure ","permalink":"https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/","summary":"In July, we merged 33 PRs! 🎉\nOn the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. 'a in for\u0026lt;'a\u0026gt; \u0026amp;'a T: PartialEq\u0026lt;i32\u0026gt;) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code.\nIn the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue.","title":"This month in hax: September 2024"},{"content":"In July, we merged 32 PRs! 🎉\nOn the side of the frontend and CLI, we had a lot of fixes and improvements! The hax command line and rustc driver were refactored, allowing for better scaling and caching. We also improved the general ergonomics: diagnostics can now be output in JSON, we have improved error messages\u0026hellip; And we pushed various bug fixes.\nIn the engine, we now resugar asserts properly and support dyn. We also pushed various enhancements (visitors for the internal AST are generated again, we propagate some more trait generics arguments\u0026hellip;) and bug fixes.\nOn the topic of libraries and helper macros, users can now add requires and ensures clauses directly on traits.\nMerged Pull Requests #811: Add mli for phase_reconstruct_for_index_loops. #802: Add json format option #800: feat(engine/ocaml_of_json_schema): add val to keyword list #799: fix(bounded-ints): zero and one were inverted #797: Fix potentially looping predicate_id. #796: Add nicer error messages when rustc emits an error in detect_forking. #795: fix: precondition constraints should be of the shape true =\u0026gt; pred #794: Resugar asserts #792: feat(frontend): Add option to control output directory #790: Allow ensures and requires on traits #788: Fix #296 #779: Support let-else pattern. #777: Small typo fixes for hax book #776: feat(book): fix checkboxes #769: Extensions to the proof-libs for libcrux-ml-kem #765: fix(engine/lib): import associated item projection on generic bounds #764: feat(hax-lib): allow requires \u0026amp; ensures on \u0026amp;mut inputs functions #763: fix(hax-lib): refinements: various fixes #762: fix(hax-lib): use super::* in refinement expansion #759: fix(frontend): crashes on fn ptr #758: fix color printing in util script #756: fix(frontend): kill crate_type in HaxMeta #753: exporter: make it need nightly only when feature rustc is on #751: Engine: propagate trait generics arguments #750: feat(exporter): thir: call: separate trait VS method generic args #744: doc(engine): ppx_functor_application #743: Refactor of the frontend #730: fix(frontend): make path_to breadth-first #729: Move book from hacspec/book to hacspec/hax #727: fix(engine): Concrete_ident_generated: name -\u0026gt; t, derive more #698: Generate visitors automatically Contributors paulmure maximebuyse karthikbhargavan W95Psp ","permalink":"https://hacspec.github.io/blog/posts/this-month-in-hax/2024-07/","summary":"In July, we merged 32 PRs! 🎉\nOn the side of the frontend and CLI, we had a lot of fixes and improvements! The hax command line and rustc driver were refactored, allowing for better scaling and caching. We also improved the general ergonomics: diagnostics can now be output in JSON, we have improved error messages\u0026hellip; And we pushed various bug fixes.\nIn the engine, we now resugar asserts properly and support dyn.","title":"This month in hax: July 2024"},{"content":"This first blog post inaugurates our series named \u0026ldquo;This Month in hax\u0026rdquo;: a series of short highlights of what happened in the development of hax and it\u0026rsquo;s ecosystem in the month.\nIn June, 23 PRs have been merged 🎉! The detail is available below.\nOn the Rust side, we have updated the Rust compiler to a very recent nightly thanks to @Nadrieril! We also added support for more Rust features in the frontend (dyn Trait), more disciminant informations on ADTs, fixed various bugs, and improved the general experience of using hax.\nWe pushed many fixes for the F* backend in the engine and improved the F* proof library. We also improved the bounded integer library and it\u0026rsquo;s F* integration.\nMerged Pull Requests Translate dyn Trait information fix(engine/fstar): use Base.String.hash instead of String.hash feat: add LICENSE Update rustc all at once refactor(engine/fstar-ast): get rid of zarith and GMP Update rustc fix(engine/fstar): fix implicit discrepancies in traits feat(nix): reduce closure size for hax-engine Generalize bounded ints Don\u0026rsquo;t use strings to represent paths Update rustc fix(backends/fstar): no __marker_trait if parent bounds feat(proof-libs): add t_Default feat(hax): logging: enable tracing in release, add trait-related logs fix(exporter): disable impl expr resolution under type aliases fix: rename action for extracting ml-kem feat: isolate DefId: faster build times fix(README): always begin relative path with ./, rewrite in action fix(ci): newer version of ppx_deriving (6.0.2) loops indefinitely Update to OCaml 5 Export discriminant values in AdtDef Update README.md Bump rustc version ","permalink":"https://hacspec.github.io/blog/posts/this-month-in-hax/2024-06/","summary":"This first blog post inaugurates our series named \u0026ldquo;This Month in hax\u0026rdquo;: a series of short highlights of what happened in the development of hax and it\u0026rsquo;s ecosystem in the month.\nIn June, 23 PRs have been merged 🎉! The detail is available below.\nOn the Rust side, we have updated the Rust compiler to a very recent nightly thanks to @Nadrieril! We also added support for more Rust features in the frontend (dyn Trait), more disciminant informations on ADTs, fixed various bugs, and improved the general experience of using hax.","title":"This month in hax: June 2024"},{"content":"We have been applying hax to verify several Rust pieces of software recently. hax was used to verify Libcrux\u0026rsquo;s implementation of ML-KEM with F*, but also for smart contracts verification with Coq, and even on protocols with F* and our new ProVerif backend.\nMeanwhile, we also presented hax at several conferences and workshops. The need for more documentation and guidance was becoming apparent: it was about time to have a tutorial!\nNew resources to learn more about hax The hax book has three new chapters:\nThe Quick start chapter explains how to go from a simple Rust crate to an F* extraction via hax, including how to install the tooling. The Tutorial chapter goes more in-depth into using hax and F* together to prove various properties of Rust code. The FAQ chapter is a work in progress but is intended to answer pragmatically and with examples to precise common issues or questions. Feel free to open an issue on the book repository if you feel like a topic should be addressed! We also added several examples of Rust verification via hax and F* in the example directory of hax, please check them out!\n","permalink":"https://hacspec.github.io/blog/posts/announcement-tutorial/","summary":"We have been applying hax to verify several Rust pieces of software recently. hax was used to verify Libcrux\u0026rsquo;s implementation of ML-KEM with F*, but also for smart contracts verification with Coq, and even on protocols with F* and our new ProVerif backend.\nMeanwhile, we also presented hax at several conferences and workshops. The need for more documentation and guidance was becoming apparent: it was about time to have a tutorial!","title":"Announcing the hax tutorial"},{"content":"This has been in the making for a while now. But we are finally happy to announce the first release of hax. It is still early days and we only tagged v0.1. But a ton of work has gone into this release.\nWait, what is hax?\nLet\u0026rsquo;s start at the beginning. A group of us started hacspec (high assurance crypto specifications), a language for specifying cryptographic primitives as the basis for formal verification, in early 2018 at the HACS workshop. After two iterations on hacspec the project outgrew the name and the initial crypto-oriented scope.\nHere comes hax. hax is a tool for high assurance translations that translates a large-ish subset of safe Rust into the formal languages accepted by proof assistants such as F* or Coq. Backends for other provers like EasyCrypt are under construction.\nThis is the result of joint work between the Prosecco team at Inria, Cryspen, and Prof. Spitters\u0026rsquo; group at Aarhus University.\nThe key design principle behind hax is hat we want to build a usable tool for verifying Rust programs without forcing the user to commit to a specific proof environment. In the future, we hope multiple tool developers will find it fruitful to build backends for hax.\nSo what is hacspec now?\nhacspec is a purely functional subset of Rust that can be used, together with a hacspec standard library, to write succinct, executable, and verifiable specifications in Rust. These specifications can be translated into formal languages with hax.\nhax There are a number of Rust verification projects out there. See, for example, Rust Verify and the Rust Formal Methods Interest Group. While most existing tools try to precisely model the most complex bits the Rust language, hax aims to be a usable and pragmatic tool that can analyze the kind of code Rust developers write on a daily basis, while abstracting away or ignoring Rust features it does not support. We believe that it is important in practice to have a usable tool that can ingest large Rust crates to show properties on certain parts of the code, instead of getting stuck on hard corner cases.\nhax has two parts: the exporter and the engine.\nThe Exporter When hax is invoked on a Rust crate, the exporter hooks into the Rust compiler. Compiling a program, Rust transformes the user source code to various internal representations in an optimized fashion (essentially HIR, THIR and MIR, illustrated in the diagram below). While this is great within the compiler, those representations are not friendly to external tool consumption.\nThe hax exporter is a Rust driver that provides a bridge from those unstable internal representations to fixed and easy-to-consume ASTs1 (abstract syntax trees). The JSON node on the diagram below represents those ASTs.\nThe hax exporter is not opinionated toward the hax project: it can be used as a frontend to the Rust compiler in other projects. For example, we are working with the Aeneas project towards sharing the exporter code between the two tools.\nThe Engine The magic of hax really happens in the engine, written in OCaml. It directly consumes2 the output of the exporter, that is, the ASTs exported for your crate of choice.\nUpon the backend choice (for instance: shall we extract to F* or to Coq?), the engine proceeds to a sequence of typed3 program transformations, eventually landing into the sublanguage supported by the targeted language, e.g. F*.\nThe various program transformations are called phases. We have a dozen of them:\ntransforming and functionalizing for loops; functionalizing local mutation; rewrite functions with mutable references as inputs into state-passing code; and many more! Those phases are statically typed: for instance, making for loops functional is not possible on an AST that still contains local mutation. Such constraints are ensured statically, reducing opportunities for bugs.\nThis typed phase design allows us to target heterogeneous languages: for instance, we already support a backend in the imperative language of the SSProve Coq library. This comes with an automatic proof that it is equivalent to the functional interpretation. This can be seen as a case-by-case correctness proof of hax.\nThis design can be used as a template for the upcoming backend which targets the imperative language of EasyCrypt.\nUsage hax is still heavily under development. It is therefore recommended to install it straight from the git repository (see the Installation section in the readme).\nAfter installing it you can call it from any Rust crate.\ncargo hax into fstar This will extract the crate to F*. Similarly, cargo hax into coq will extract the crate to Coq.\nFor more options use\ncargo hax into --help Example We walk through a sample usage of hax based on an example. The example can be found in the git repository.\nGo to the proofs/fstar/extraction directory and run make. This will first call\ncargo hax into -i \u0026#39;-** +**::process_order\u0026#39; fstar in order to extract the process_order order function to F*. This demonstrates one particularly useful feature in hax, which allows extracting only a small portion or single function from a much larger crate. The argument -i '-** +**::process_order' tells hax to include the process_order function in any module and exclude (-**) everything else. In addition to the function itself, hax extracts all the required dependencies within the crate as well.\nRust fn process_order\u0026lt;T\u0026gt;(mut order: Order, other_side: \u0026amp;mut BinaryHeap\u0026lt;T\u0026gt;) -\u0026gt; (Vec\u0026lt;Match\u0026gt;, Option\u0026lt;Order\u0026gt;) where T: Into\u0026lt;Order\u0026gt; + From\u0026lt;Order\u0026gt; + Ord + Clone, { ... if let Some(m) = other_side .peek() .and_then(|other| Into::into(other.clone()).try_match(\u0026amp;order)) { order.quantity -= m.quantity; let mut other: Order = Into::into(other_side.pop().unwrap()); other.quantity -= m.quantity; if other.quantity \u0026gt; 0 { other_side.push(From::from(other.clone())); } matches.push(m); } else { done = true; } ... } F* match Core.Option.impl__and_then (Alloc.Collections.Binary_heap.impl_10__peek other_side \u0026lt;: Core.Option.t_Option v_T) (fun other -\u0026gt; impl__Order__try_match (Core.Convert.f_into (Core.Clone.f_clone other \u0026lt;: v_T) \u0026lt;: t_Order) order \u0026lt;: Core.Option.t_Option t_Match) \u0026lt;: Core.Option.t_Option t_Match with | Core.Option.Option_Some m -\u0026gt; let order:t_Order = { order with f_quantity = order.f_quantity -! m.f_quantity } in let tmp0, out:(Alloc.Collections.Binary_heap.t_BinaryHeap v_T \u0026amp; Core.Option.t_Option v_T) = Alloc.Collections.Binary_heap.impl_9__pop other_side in let other_side:Alloc.Collections.Binary_heap.t_BinaryHeap v_T = tmp0 in let hoist1:Core.Option.t_Option v_T = out in let hoist2:v_T = Core.Option.impl__unwrap hoist1 in let (other: t_Order):t_Order = Core.Convert.f_into hoist2 in let other:t_Order = { other with f_quantity = other.f_quantity -! m.f_quantity } in let other_side:Alloc.Collections.Binary_heap.t_BinaryHeap v_T = if other.f_quantity \u0026gt;. 0uL then let other_side:Alloc.Collections.Binary_heap.t_BinaryHeap v_T = Alloc.Collections.Binary_heap.impl_9__push other_side (Core.Convert.f_from (Core.Clone.f_clone other \u0026lt;: t_Order) \u0026lt;: v_T) in other_side else other_side in let matches:Alloc.Vec.t_Vec t_Match Alloc.Alloc.t_Global = Alloc.Vec.impl_1__push matches m in done, matches, order, other_side | _ -\u0026gt; let done:bool = true in done, matches, order, other_side Then the makefile calls F* on the generated output. The successful typechecking in F* proves two properties on the Rust code.\nNon-panicking subtraction First, it shows that the lines with\norder.quantity -= m.quantity; do not underflow.\nConcretely, in Rust, the subtraction on u64 integers is a partial operation: the subtraction of x and y (x - y) is defined only when x is greater or equal to y such that x - y \u0026gt;= 0.\nSuch a requirement cannot be expressed as a Rust type, thus Rust\u0026rsquo;s subtraction panics (in debug mode) when it is called with bad inputs.\nIn contrast, F* is ideal to express such types! We model Rust\u0026rsquo;s subtraction as a total function with a strong type signature:\nval ( -! ): x: u64 -\u0026gt; y: u64 {x \u0026gt;=. y} -\u0026gt; u64 This strong signature implies a proof obligation: whenever this F* subtraction is used, F* won\u0026rsquo;t typecheck unless it finds a proof that x \u0026gt;=. y holds.\nTherefore, typechecking in F* implies that order.quantity -= m.quantity; never underflows.\nNon-panicking unwrap Second, it shows that\nother_side.pop().unwrap() never panics, i.e. the pop always returns Some value and thus unwrap never panics.\nSimilarly to subtraction, in F*, using unwrap requires a proof that the option being unwrapped is not None.\nCall to Action hax is still under heavy development and there are many features we want to add, and many bugs to squash. We invite everyone to contribute to the project with new backends, contributing to the hax frontend or backend, or provide examples to exercise the tool.\nThe F* backend is currently being developed by the Inria Prosecco team, the Coq backend by the Aarhus team, and an EasyCrypt backend is in the works by the EasyCrypt team. We are also working with the Aeneas project to allow better interoperability between their sophisticated stateful Rust verification toolchain and hax.\nResources Zulip Git Repository Rust\u0026rsquo;s internal ASTs are very optimized in memory and require constantly to lookup things interactively with the Rust compiler. Instead, our ASTs are indirection-free trees packing as much informations as possible (e.g. types, attributes, spans\u0026hellip;), ready for direct consumption.\u0026#160;\u0026#x21a9;\u0026#xfe0e;\nThe exporter expose big ASTs as JSON. The Rust type definitions of those ASTs are automatically converted into OCaml type definition along with JSON serializer and deserializers, using JSON Schemas.\u0026#160;\u0026#x21a9;\u0026#xfe0e;\nThe internal AST used by the hax engine is functorized. This enables AST transformations to be strongly typed.\u0026#160;\u0026#x21a9;\u0026#xfe0e;\n","permalink":"https://hacspec.github.io/blog/posts/hax-v0-1/","summary":"This has been in the making for a while now. But we are finally happy to announce the first release of hax. It is still early days and we only tagged v0.1. But a ton of work has gone into this release.\nWait, what is hax?\nLet\u0026rsquo;s start at the beginning. A group of us started hacspec (high assurance crypto specifications), a language for specifying cryptographic primitives as the basis for formal verification, in early 2018 at the HACS workshop.","title":"Introducing hax 🎂"}]
\ No newline at end of file
diff --git a/index.xml b/index.xml
index 27a3812..68575f8 100644
--- a/index.xml
+++ b/index.xml
@@ -11,7 +11,18 @@
     </image>
     <generator>Hugo -- gohugo.io</generator>
     <language>en</language>
-    <lastBuildDate>Mon, 12 Aug 2024 00:00:00 +0000</lastBuildDate><atom:link href="https://hacspec.github.io/blog/index.xml" rel="self" type="application/rss+xml" />
+    <lastBuildDate>Tue, 01 Oct 2024 00:00:00 +0000</lastBuildDate><atom:link href="https://hacspec.github.io/blog/index.xml" rel="self" type="application/rss+xml" />
+    <item>
+      <title>This month in hax: September 2024</title>
+      <link>https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/</link>
+      <pubDate>Tue, 01 Oct 2024 00:00:00 +0000</pubDate>
+      
+      <guid>https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/</guid>
+      <description>In July, we merged 33 PRs! 🎉
+On the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. &#39;a in for&amp;lt;&#39;a&amp;gt; &amp;amp;&#39;a T: PartialEq&amp;lt;i32&amp;gt;) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code.
+In the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue.</description>
+    </item>
+    
     <item>
       <title>This month in hax: July 2024</title>
       <link>https://hacspec.github.io/blog/posts/this-month-in-hax/2024-07/</link>
diff --git a/posts/index.html b/posts/index.html
index 8238460..c1f5e92 100644
--- a/posts/index.html
+++ b/posts/index.html
@@ -1,6 +1,8 @@
 <!doctype html><html lang=en dir=auto><head><meta charset=utf-8><meta http-equiv=X-UA-Compatible content="IE=edge"><meta name=viewport content="width=device-width,initial-scale=1,shrink-to-fit=no"><meta name=robots content="index, follow"><title>Posts | hax</title>
 <meta name=keywords content><meta name=description content="Posts - hax"><meta name=author content="hacspec authors"><link rel=canonical href=https://hacspec.github.io/blog/posts/><link crossorigin=anonymous href=/blog/assets/css/stylesheet.1b82bbed8b13f853704558d527b681efaea938ce91e6ae8903e8b19e73b1b0f8.css integrity="sha256-G4K77YsT+FNwRVjVJ7aB766pOM6R5q6JA+ixnnOxsPg=" rel="preload stylesheet" as=style><link rel=icon href=https://hacspec.github.io/blog/favicon.ico><link rel=icon type=image/png sizes=16x16 href=https://hacspec.github.io/blog/favicon-16x16.png><link rel=icon type=image/png sizes=32x32 href=https://hacspec.github.io/blog/favicon-32x32.png><link rel=apple-touch-icon href=https://hacspec.github.io/blog/apple-touch-icon.png><link rel=mask-icon href=https://hacspec.github.io/blog/safari-pinned-tab.svg><meta name=theme-color content="#2e2e33"><meta name=msapplication-TileColor content="#2e2e33"><link rel=alternate type=application/rss+xml href=https://hacspec.github.io/blog/posts/index.xml><noscript><style>#theme-toggle,.top-link{display:none}</style><style>@media(prefers-color-scheme:dark){:root{--theme:rgb(29, 30, 32);--entry:rgb(46, 46, 51);--primary:rgb(218, 218, 219);--secondary:rgb(155, 156, 157);--tertiary:rgb(65, 66, 68);--content:rgb(196, 196, 197);--hljs-bg:rgb(46, 46, 51);--code-bg:rgb(55, 56, 62);--border:rgb(51, 51, 51)}.list{background:var(--theme)}.list:not(.dark)::-webkit-scrollbar-track{background:0 0}.list:not(.dark)::-webkit-scrollbar-thumb{border-color:var(--theme)}}</style></noscript><meta property="og:title" content="Posts"><meta property="og:description" content="hax & hacspec blog - https://github.com/hacspec/blog"><meta property="og:type" content="website"><meta property="og:url" content="https://hacspec.github.io/blog/posts/"><meta property="og:image" content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:card content="summary_large_image"><meta name=twitter:image content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:title content="Posts"><meta name=twitter:description content="hax & hacspec blog - https://github.com/hacspec/blog"><script type=application/ld+json>{"@context":"https://schema.org","@type":"BreadcrumbList","itemListElement":[{"@type":"ListItem","position":1,"name":"Posts","item":"https://hacspec.github.io/blog/posts/"}]}</script></head><body class=list id=top><script>localStorage.getItem("pref-theme")==="dark"?document.body.classList.add("dark"):localStorage.getItem("pref-theme")==="light"?document.body.classList.remove("dark"):window.matchMedia("(prefers-color-scheme: dark)").matches&&document.body.classList.add("dark")</script><header class=header><nav class=nav><div class=logo><a href=https://hacspec.github.io/blog/ accesskey=h title="hax (Alt + H)">hax</a><div class=logo-switches><button id=theme-toggle accesskey=t title="(Alt + T)"><svg id="moon" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M21 12.79A9 9 0 1111.21 3 7 7 0 0021 12.79z"/></svg><svg id="sun" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><circle cx="12" cy="12" r="5"/><line x1="12" y1="1" x2="12" y2="3"/><line x1="12" y1="21" x2="12" y2="23"/><line x1="4.22" y1="4.22" x2="5.64" y2="5.64"/><line x1="18.36" y1="18.36" x2="19.78" y2="19.78"/><line x1="1" y1="12" x2="3" y2="12"/><line x1="21" y1="12" x2="23" y2="12"/><line x1="4.22" y1="19.78" x2="5.64" y2="18.36"/><line x1="18.36" y1="5.64" x2="19.78" y2="4.22"/></svg></button></div></div><ul id=menu><li><a href=https://hacspec.github.io/blog/archives title=Archive><span>Archive</span></a></li><li><a href=https://hacspec.github.io/blog/search/ title="Search (Alt + /)" accesskey=/><span>Search</span></a></li><li><a href=https://hacspec.github.io/blog/tags/ title=Tags><span>Tags</span></a></li></ul></nav></header><main class=main><header class=page-header><div class=breadcrumbs><a href=https://hacspec.github.io/blog/>Home</a></div><h1>Posts
-<a href=/blog/posts/index.xml title=RSS aria-label=RSS><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" height="23"><path d="M4 11a9 9 0 019 9"/><path d="M4 4a16 16 0 0116 16"/><circle cx="5" cy="19" r="1"/></svg></a></h1></header><article class=post-entry><header class=entry-header><h2>This month in hax: July 2024</h2></header><div class=entry-content><p>In July, we merged 32 PRs! 🎉
+<a href=/blog/posts/index.xml title=RSS aria-label=RSS><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" height="23"><path d="M4 11a9 9 0 019 9"/><path d="M4 4a16 16 0 0116 16"/><circle cx="5" cy="19" r="1"/></svg></a></h1></header><article class=post-entry><header class=entry-header><h2>This month in hax: September 2024</h2></header><div class=entry-content><p>In July, we merged 33 PRs! 🎉
+On the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. 'a in for&lt;'a> &'a T: PartialEq&lt;i32>) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code.
+In the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue....</p></div><footer class=entry-footer><span title='2024-10-01 00:00:00 +0000 UTC'>October 1, 2024</span>&nbsp;·&nbsp;2 min&nbsp;·&nbsp;Lucas Franceschino</footer><a class=entry-link aria-label="post link to This month in hax: September 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/></a></article><article class=post-entry><header class=entry-header><h2>This month in hax: July 2024</h2></header><div class=entry-content><p>In July, we merged 32 PRs! 🎉
 On the side of the frontend and CLI, we had a lot of fixes and improvements! The hax command line and rustc driver were refactored, allowing for better scaling and caching. We also improved the general ergonomics: diagnostics can now be output in JSON, we have improved error messages… And we pushed various bug fixes.
 In the engine, we now resugar asserts properly and support dyn....</p></div><footer class=entry-footer><span title='2024-08-12 00:00:00 +0000 UTC'>August 12, 2024</span>&nbsp;·&nbsp;2 min&nbsp;·&nbsp;Lucas Franceschino</footer><a class=entry-link aria-label="post link to This month in hax: July 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-07/></a></article><article class=post-entry><header class=entry-header><h2>This month in hax: June 2024</h2></header><div class=entry-content><p>This first blog post inaugurates our series named “This Month in hax”: a series of short highlights of what happened in the development of hax and it’s ecosystem in the month.
 In June, 23 PRs have been merged 🎉! The detail is available below.
diff --git a/posts/index.xml b/posts/index.xml
index c0c9111..7d6b26c 100644
--- a/posts/index.xml
+++ b/posts/index.xml
@@ -11,7 +11,18 @@
     </image>
     <generator>Hugo -- gohugo.io</generator>
     <language>en</language>
-    <lastBuildDate>Mon, 12 Aug 2024 00:00:00 +0000</lastBuildDate><atom:link href="https://hacspec.github.io/blog/posts/index.xml" rel="self" type="application/rss+xml" />
+    <lastBuildDate>Tue, 01 Oct 2024 00:00:00 +0000</lastBuildDate><atom:link href="https://hacspec.github.io/blog/posts/index.xml" rel="self" type="application/rss+xml" />
+    <item>
+      <title>This month in hax: September 2024</title>
+      <link>https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/</link>
+      <pubDate>Tue, 01 Oct 2024 00:00:00 +0000</pubDate>
+      
+      <guid>https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/</guid>
+      <description>In July, we merged 33 PRs! 🎉
+On the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. &#39;a in for&amp;lt;&#39;a&amp;gt; &amp;amp;&#39;a T: PartialEq&amp;lt;i32&amp;gt;) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code.
+In the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue.</description>
+    </item>
+    
     <item>
       <title>This month in hax: July 2024</title>
       <link>https://hacspec.github.io/blog/posts/this-month-in-hax/2024-07/</link>
diff --git a/posts/this-month-in-hax/2024-07/index.html b/posts/this-month-in-hax/2024-07/index.html
index f6682ee..ff90d75 100644
--- a/posts/this-month-in-hax/2024-07/index.html
+++ b/posts/this-month-in-hax/2024-07/index.html
@@ -19,7 +19,8 @@
 generated again, we propagate some more trait generics arguments&mldr;)
 and bug fixes.</p><p>On the topic of libraries and helper macros, users can <a href=https://github.com/hacspec/hax/pull/790>now add
 <code>requires</code> and <code>ensures</code>
-clauses</a> directly on traits.</p><h1 id=merged-pull-requests>Merged Pull Requests<a hidden class=anchor aria-hidden=true href=#merged-pull-requests>#</a></h1><ul><li>#811: <a href=https://github.com/hacspec/hax/pull/811>Add mli for phase_reconstruct_for_index_loops.</a></li><li>#802: <a href=https://github.com/hacspec/hax/pull/802>Add json format option</a></li><li>#800: <a href=https://github.com/hacspec/hax/pull/800>feat(engine/ocaml_of_json_schema): add <code>val</code> to keyword list</a></li><li>#799: <a href=https://github.com/hacspec/hax/pull/799>fix(bounded-ints): zero and one were inverted</a></li><li>#797: <a href=https://github.com/hacspec/hax/pull/797>Fix potentially looping predicate_id.</a></li><li>#796: <a href=https://github.com/hacspec/hax/pull/796>Add nicer error messages when rustc emits an error in detect_forking.</a></li><li>#795: <a href=https://github.com/hacspec/hax/pull/795>fix: precondition constraints should be of the shape <code>true => pred</code></a></li><li>#794: <a href=https://github.com/hacspec/hax/pull/794>Resugar asserts</a></li><li>#792: <a href=https://github.com/hacspec/hax/pull/792>feat(frontend): Add option to control output directory</a></li><li>#790: <a href=https://github.com/hacspec/hax/pull/790>Allow <code>ensures</code> and <code>requires</code> on traits</a></li><li>#788: <a href=https://github.com/hacspec/hax/pull/788>Fix #296</a></li><li>#779: <a href=https://github.com/hacspec/hax/pull/779>Support let-else pattern.</a></li><li>#777: <a href=https://github.com/hacspec/hax/pull/777>Small typo fixes for hax book</a></li><li>#776: <a href=https://github.com/hacspec/hax/pull/776>feat(book): fix checkboxes</a></li><li>#769: <a href=https://github.com/hacspec/hax/pull/769>Extensions to the proof-libs for libcrux-ml-kem</a></li><li>#765: <a href=https://github.com/hacspec/hax/pull/765>fix(engine/lib): import associated item projection on generic bounds</a></li><li>#764: <a href=https://github.com/hacspec/hax/pull/764>feat(hax-lib): allow requires & ensures on <code>&amp;mut</code> inputs functions</a></li><li>#763: <a href=https://github.com/hacspec/hax/pull/763>fix(hax-lib): refinements: various fixes</a></li><li>#762: <a href=https://github.com/hacspec/hax/pull/762>fix(hax-lib): <code>use super::*</code> in refinement expansion</a></li><li>#759: <a href=https://github.com/hacspec/hax/pull/759>fix(frontend): crashes on fn ptr</a></li><li>#758: <a href=https://github.com/hacspec/hax/pull/758>fix color printing in util script</a></li><li>#756: <a href=https://github.com/hacspec/hax/pull/756>fix(frontend): kill <code>crate_type</code> in <code>HaxMeta</code></a></li><li>#753: <a href=https://github.com/hacspec/hax/pull/753>exporter: make it need nightly only when feature <code>rustc</code> is on</a></li><li>#751: <a href=https://github.com/hacspec/hax/pull/751>Engine: propagate trait generics arguments</a></li><li>#750: <a href=https://github.com/hacspec/hax/pull/750>feat(exporter): thir: call: separate trait VS method generic args</a></li><li>#744: <a href=https://github.com/hacspec/hax/pull/744>doc(engine): ppx_functor_application</a></li><li>#743: <a href=https://github.com/hacspec/hax/pull/743>Refactor of the frontend</a></li><li>#730: <a href=https://github.com/hacspec/hax/pull/730>fix(frontend): make <code>path_to</code> breadth-first</a></li><li>#729: <a href=https://github.com/hacspec/hax/pull/729>Move book from <code>hacspec/book</code> to <code>hacspec/hax</code></a></li><li>#727: <a href=https://github.com/hacspec/hax/pull/727>fix(engine): <code>Concrete_ident_generated</code>: <code>name</code> -> <code>t</code>, derive more</a></li><li>#698: <a href=https://github.com/hacspec/hax/pull/698>Generate visitors automatically</a></li></ul><h1 id=contributors>Contributors<a hidden class=anchor aria-hidden=true href=#contributors>#</a></h1><ul><li><a href=https://github.com/paulmure>paulmure</a></li><li><a href=https://github.com/maximebuyse>maximebuyse</a></li><li><a href=https://github.com/karthikbhargavan>karthikbhargavan</a></li><li><a href=https://github.com/W95Psp>W95Psp</a></li></ul></div><footer class=post-footer><ul class=post-tags><li><a href=https://hacspec.github.io/blog/tags/this-month-in-hax/>this-month-in-hax</a></li></ul><nav class=paginav><a class=next href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-06/><span class=title>Next »</span><br><span>This month in hax: June 2024</span></a></nav></footer></article></main><footer class=footer><span>&copy; 2024 <a href=https://hacspec.github.io/blog/>hax</a></span>
+clauses</a> directly on traits.</p><h1 id=merged-pull-requests>Merged Pull Requests<a hidden class=anchor aria-hidden=true href=#merged-pull-requests>#</a></h1><ul><li>#811: <a href=https://github.com/hacspec/hax/pull/811>Add mli for phase_reconstruct_for_index_loops.</a></li><li>#802: <a href=https://github.com/hacspec/hax/pull/802>Add json format option</a></li><li>#800: <a href=https://github.com/hacspec/hax/pull/800>feat(engine/ocaml_of_json_schema): add <code>val</code> to keyword list</a></li><li>#799: <a href=https://github.com/hacspec/hax/pull/799>fix(bounded-ints): zero and one were inverted</a></li><li>#797: <a href=https://github.com/hacspec/hax/pull/797>Fix potentially looping predicate_id.</a></li><li>#796: <a href=https://github.com/hacspec/hax/pull/796>Add nicer error messages when rustc emits an error in detect_forking.</a></li><li>#795: <a href=https://github.com/hacspec/hax/pull/795>fix: precondition constraints should be of the shape <code>true => pred</code></a></li><li>#794: <a href=https://github.com/hacspec/hax/pull/794>Resugar asserts</a></li><li>#792: <a href=https://github.com/hacspec/hax/pull/792>feat(frontend): Add option to control output directory</a></li><li>#790: <a href=https://github.com/hacspec/hax/pull/790>Allow <code>ensures</code> and <code>requires</code> on traits</a></li><li>#788: <a href=https://github.com/hacspec/hax/pull/788>Fix #296</a></li><li>#779: <a href=https://github.com/hacspec/hax/pull/779>Support let-else pattern.</a></li><li>#777: <a href=https://github.com/hacspec/hax/pull/777>Small typo fixes for hax book</a></li><li>#776: <a href=https://github.com/hacspec/hax/pull/776>feat(book): fix checkboxes</a></li><li>#769: <a href=https://github.com/hacspec/hax/pull/769>Extensions to the proof-libs for libcrux-ml-kem</a></li><li>#765: <a href=https://github.com/hacspec/hax/pull/765>fix(engine/lib): import associated item projection on generic bounds</a></li><li>#764: <a href=https://github.com/hacspec/hax/pull/764>feat(hax-lib): allow requires & ensures on <code>&amp;mut</code> inputs functions</a></li><li>#763: <a href=https://github.com/hacspec/hax/pull/763>fix(hax-lib): refinements: various fixes</a></li><li>#762: <a href=https://github.com/hacspec/hax/pull/762>fix(hax-lib): <code>use super::*</code> in refinement expansion</a></li><li>#759: <a href=https://github.com/hacspec/hax/pull/759>fix(frontend): crashes on fn ptr</a></li><li>#758: <a href=https://github.com/hacspec/hax/pull/758>fix color printing in util script</a></li><li>#756: <a href=https://github.com/hacspec/hax/pull/756>fix(frontend): kill <code>crate_type</code> in <code>HaxMeta</code></a></li><li>#753: <a href=https://github.com/hacspec/hax/pull/753>exporter: make it need nightly only when feature <code>rustc</code> is on</a></li><li>#751: <a href=https://github.com/hacspec/hax/pull/751>Engine: propagate trait generics arguments</a></li><li>#750: <a href=https://github.com/hacspec/hax/pull/750>feat(exporter): thir: call: separate trait VS method generic args</a></li><li>#744: <a href=https://github.com/hacspec/hax/pull/744>doc(engine): ppx_functor_application</a></li><li>#743: <a href=https://github.com/hacspec/hax/pull/743>Refactor of the frontend</a></li><li>#730: <a href=https://github.com/hacspec/hax/pull/730>fix(frontend): make <code>path_to</code> breadth-first</a></li><li>#729: <a href=https://github.com/hacspec/hax/pull/729>Move book from <code>hacspec/book</code> to <code>hacspec/hax</code></a></li><li>#727: <a href=https://github.com/hacspec/hax/pull/727>fix(engine): <code>Concrete_ident_generated</code>: <code>name</code> -> <code>t</code>, derive more</a></li><li>#698: <a href=https://github.com/hacspec/hax/pull/698>Generate visitors automatically</a></li></ul><h1 id=contributors>Contributors<a hidden class=anchor aria-hidden=true href=#contributors>#</a></h1><ul><li><a href=https://github.com/paulmure>paulmure</a></li><li><a href=https://github.com/maximebuyse>maximebuyse</a></li><li><a href=https://github.com/karthikbhargavan>karthikbhargavan</a></li><li><a href=https://github.com/W95Psp>W95Psp</a></li></ul></div><footer class=post-footer><ul class=post-tags><li><a href=https://hacspec.github.io/blog/tags/this-month-in-hax/>this-month-in-hax</a></li></ul><nav class=paginav><a class=prev href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/><span class=title>« Prev</span><br><span>This month in hax: September 2024</span>
+</a><a class=next href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-06/><span class=title>Next »</span><br><span>This month in hax: June 2024</span></a></nav></footer></article></main><footer class=footer><span>&copy; 2024 <a href=https://hacspec.github.io/blog/>hax</a></span>
 <span>Powered by
 <a href=https://gohugo.io/ rel="noopener noreferrer" target=_blank>Hugo</a> &
         <a href=https://github.com/adityatelange/hugo-PaperMod/ rel=noopener target=_blank>PaperMod</a></span></footer><a href=#top aria-label="go to top" title="Go to Top (Alt + G)" class=top-link id=top-link accesskey=g><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 12 6" fill="currentcolor"><path d="M12 6H0l6-6z"/></svg></a><script>let menu=document.getElementById("menu");menu&&(menu.scrollLeft=localStorage.getItem("menu-scroll-position"),menu.onscroll=function(){localStorage.setItem("menu-scroll-position",menu.scrollLeft)}),document.querySelectorAll('a[href^="#"]').forEach(e=>{e.addEventListener("click",function(e){e.preventDefault();var t=this.getAttribute("href").substr(1);window.matchMedia("(prefers-reduced-motion: reduce)").matches?document.querySelector(`[id='${decodeURIComponent(t)}']`).scrollIntoView():document.querySelector(`[id='${decodeURIComponent(t)}']`).scrollIntoView({behavior:"smooth"}),t==="top"?history.replaceState(null,null," "):history.pushState(null,null,`#${t}`)})})</script><script>var mybutton=document.getElementById("top-link");window.onscroll=function(){document.body.scrollTop>800||document.documentElement.scrollTop>800?(mybutton.style.visibility="visible",mybutton.style.opacity="1"):(mybutton.style.visibility="hidden",mybutton.style.opacity="0")}</script><script>document.getElementById("theme-toggle").addEventListener("click",()=>{document.body.className.includes("dark")?(document.body.classList.remove("dark"),localStorage.setItem("pref-theme","light")):(document.body.classList.add("dark"),localStorage.setItem("pref-theme","dark"))})</script><script>document.querySelectorAll("pre > code").forEach(e=>{const n=e.parentNode.parentNode,t=document.createElement("button");t.classList.add("copy-code"),t.innerHTML="copy";function s(){t.innerHTML="copied!",setTimeout(()=>{t.innerHTML="copy"},2e3)}t.addEventListener("click",t=>{if("clipboard"in navigator){navigator.clipboard.writeText(e.textContent),s();return}const n=document.createRange();n.selectNodeContents(e);const o=window.getSelection();o.removeAllRanges(),o.addRange(n);try{document.execCommand("copy"),s()}catch{}o.removeRange(n)}),n.classList.contains("highlight")?n.appendChild(t):n.parentNode.firstChild==n||(e.parentNode.parentNode.parentNode.parentNode.parentNode.nodeName=="TABLE"?e.parentNode.parentNode.parentNode.parentNode.parentNode.appendChild(t):e.parentNode.appendChild(t))})</script></body></html>
\ No newline at end of file
diff --git a/posts/this-month-in-hax/2024-09/index.html b/posts/this-month-in-hax/2024-09/index.html
new file mode 100644
index 0000000..7afb22f
--- /dev/null
+++ b/posts/this-month-in-hax/2024-09/index.html
@@ -0,0 +1,24 @@
+<!doctype html><html lang=en dir=auto><head><meta charset=utf-8><meta http-equiv=X-UA-Compatible content="IE=edge"><meta name=viewport content="width=device-width,initial-scale=1,shrink-to-fit=no"><meta name=robots content="index, follow"><title>This month in hax: September 2024 | hax</title>
+<meta name=keywords content="this-month-in-hax"><meta name=description content="In July, we merged 33 PRs! 🎉
+On the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. 'a in for<'a> &'a T: PartialEq<i32>) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code.
+In the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue."><meta name=author content="Lucas Franceschino"><link rel=canonical href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/><link crossorigin=anonymous href=/blog/assets/css/stylesheet.1b82bbed8b13f853704558d527b681efaea938ce91e6ae8903e8b19e73b1b0f8.css integrity="sha256-G4K77YsT+FNwRVjVJ7aB766pOM6R5q6JA+ixnnOxsPg=" rel="preload stylesheet" as=style><link rel=icon href=https://hacspec.github.io/blog/favicon.ico><link rel=icon type=image/png sizes=16x16 href=https://hacspec.github.io/blog/favicon-16x16.png><link rel=icon type=image/png sizes=32x32 href=https://hacspec.github.io/blog/favicon-32x32.png><link rel=apple-touch-icon href=https://hacspec.github.io/blog/apple-touch-icon.png><link rel=mask-icon href=https://hacspec.github.io/blog/safari-pinned-tab.svg><meta name=theme-color content="#2e2e33"><meta name=msapplication-TileColor content="#2e2e33"><noscript><style>#theme-toggle,.top-link{display:none}</style><style>@media(prefers-color-scheme:dark){:root{--theme:rgb(29, 30, 32);--entry:rgb(46, 46, 51);--primary:rgb(218, 218, 219);--secondary:rgb(155, 156, 157);--tertiary:rgb(65, 66, 68);--content:rgb(196, 196, 197);--hljs-bg:rgb(46, 46, 51);--code-bg:rgb(55, 56, 62);--border:rgb(51, 51, 51)}.list{background:var(--theme)}.list:not(.dark)::-webkit-scrollbar-track{background:0 0}.list:not(.dark)::-webkit-scrollbar-thumb{border-color:var(--theme)}}</style></noscript><meta property="og:title" content="This month in hax: September 2024"><meta property="og:description" content="In July, we merged 33 PRs! 🎉
+On the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. 'a in for<'a> &'a T: PartialEq<i32>) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code.
+In the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue."><meta property="og:type" content="article"><meta property="og:url" content="https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/"><meta property="og:image" content="https://hacspec.github.io/blog/papermod-cover.png"><meta property="article:section" content="posts"><meta property="article:published_time" content="2024-10-01T00:00:00+00:00"><meta property="article:modified_time" content="2024-10-01T00:00:00+00:00"><meta name=twitter:card content="summary_large_image"><meta name=twitter:image content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:title content="This month in hax: September 2024"><meta name=twitter:description content="In July, we merged 33 PRs! 🎉
+On the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. 'a in for<'a> &'a T: PartialEq<i32>) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code.
+In the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue."><script type=application/ld+json>{"@context":"https://schema.org","@type":"BreadcrumbList","itemListElement":[{"@type":"ListItem","position":1,"name":"Posts","item":"https://hacspec.github.io/blog/posts/"},{"@type":"ListItem","position":2,"name":"This month in hax: September 2024","item":"https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/"}]}</script><script type=application/ld+json>{"@context":"https://schema.org","@type":"BlogPosting","headline":"This month in hax: September 2024","name":"This month in hax: September 2024","description":"In July, we merged 33 PRs! 🎉\nOn the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. 'a in for\u0026lt;'a\u0026gt; \u0026amp;'a T: PartialEq\u0026lt;i32\u0026gt;) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code.\nIn the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue.","keywords":["this-month-in-hax"],"articleBody":"In July, we merged 33 PRs! 🎉\nOn the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. 'a in for\u003c'a\u003e \u0026'a T: PartialEq) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code.\nIn the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue.\nWe’ve been improving F* support and F* libraries. Importantly, cmester0 is working on a model of core, in Rust: we aim at replacing our hand-crafted F* model of core by an hax extraction of this new core model implemented in Rust. We will also be able to extract this model of core in every of our backends, enabling a uniform and pain-free core multi-backend library.\nMerged Pull Requests #934: chore: assign an issue id for every error in the engine #932: chore: assign an issue for every error in import_thir #919: fix #422 #918: chore: remove stale Hax.Lib.fst #917: doc: disambiguate_local_idents #916: update Cargo.lock #909: Revert “fix(engine/fstar): fix super typeclasses attributes” #908: fix(engine/deps): stop re-computing over and over the set of assoc items #907: Add RewriteControlFlow phase. #906: Cleanup trait resolution #902: fix(engine/fstar): fix super typeclasses attributes #901: Determine emuerate value by index #898: Fix some binder-related crashes #895: Don’t eval constants eagerly #894: Detangle trait solving from SInto #892: Support other variants of MIR #891: fix: fstar: default trait #887: Initial cleanup of binders-related code #885: docs(book): depend on hax-lib only when using hax #884: Fix incorrect line numbers in error messages #883: Fix step boundaries in fold_range_step_by #882: fix(fstar-core): add support for Option::map #880: Support float literals #877: Avoid recursing twice on the arguments. #876: Translate additional unsafe MIR operations #873: Small PR to fix circularity in Core.Fmt.fsti #872: Pre post impl blocks #870: count-ones post-condition #868: engine: kill a few exn to get useful errors #867: Backend: Import unsafe code as a gated feature #860: fix(engine): make dep. analysis sensible to UID assoc. items #827: Add infos impl #819: Add Rust Core Fstar Definitions. Contributors Nadrieril R1kM ROMemories W95Psp franziskuskiefer gaetan-sbt karthikbhargavan mamonet maximebuyse paulmure ","wordCount":"383","inLanguage":"en","datePublished":"2024-10-01T00:00:00Z","dateModified":"2024-10-01T00:00:00Z","author":{"@type":"Person","name":"Lucas Franceschino"},"mainEntityOfPage":{"@type":"WebPage","@id":"https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/"},"publisher":{"@type":"Organization","name":"hax","logo":{"@type":"ImageObject","url":"https://hacspec.github.io/blog/favicon.ico"}}}</script></head><body id=top><script>localStorage.getItem("pref-theme")==="dark"?document.body.classList.add("dark"):localStorage.getItem("pref-theme")==="light"?document.body.classList.remove("dark"):window.matchMedia("(prefers-color-scheme: dark)").matches&&document.body.classList.add("dark")</script><header class=header><nav class=nav><div class=logo><a href=https://hacspec.github.io/blog/ accesskey=h title="hax (Alt + H)">hax</a><div class=logo-switches><button id=theme-toggle accesskey=t title="(Alt + T)"><svg id="moon" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M21 12.79A9 9 0 1111.21 3 7 7 0 0021 12.79z"/></svg><svg id="sun" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><circle cx="12" cy="12" r="5"/><line x1="12" y1="1" x2="12" y2="3"/><line x1="12" y1="21" x2="12" y2="23"/><line x1="4.22" y1="4.22" x2="5.64" y2="5.64"/><line x1="18.36" y1="18.36" x2="19.78" y2="19.78"/><line x1="1" y1="12" x2="3" y2="12"/><line x1="21" y1="12" x2="23" y2="12"/><line x1="4.22" y1="19.78" x2="5.64" y2="18.36"/><line x1="18.36" y1="5.64" x2="19.78" y2="4.22"/></svg></button></div></div><ul id=menu><li><a href=https://hacspec.github.io/blog/archives title=Archive><span>Archive</span></a></li><li><a href=https://hacspec.github.io/blog/search/ title="Search (Alt + /)" accesskey=/><span>Search</span></a></li><li><a href=https://hacspec.github.io/blog/tags/ title=Tags><span>Tags</span></a></li></ul></nav></header><main class=main><article class=post-single><header class=post-header><h1 class=post-title>This month in hax: September 2024</h1><div class=post-meta><span title='2024-10-01 00:00:00 +0000 UTC'>October 1, 2024</span>&nbsp;·&nbsp;2 min&nbsp;·&nbsp;Lucas Franceschino</div></header><div class=post-content><p>In July, we merged 33 PRs! 🎉</p><p>On the side of the frontend, <a href=https://github.com/Nadrieril>Nadrieril</a>
+and I worked at making hax handling of binders (e.g. <code>'a</code> in <code>for&lt;'a> &'a T: PartialEq&lt;i32></code>) and traits better. This is not finished yet,
+but we made great progress. Our goal is to make the frontend work on
+every valid Rust code.</p><p>In the engine, thanks to <a href=https://github.com/paulmure>paulmure</a>, we
+now are able to process <code>unsafe</code> blocks. Thanks to
+<a href=https://github.com/maximebuyse>maximebuyse</a>, the engine can now
+rewrite more <code>return</code> expressions: we are now planning on supporting
+<code>return</code> inside loops, along with <code>break</code> and <code>continue</code>.</p><p>We&rsquo;ve been improving F* support and F* libraries. Importantly,
+<a href=https://github.com/cmester0>cmester0</a> is working on a model of
+<code>core</code>, in Rust: we aim at replacing our hand-crafted F* model of core
+by an hax extraction of this new core model implemented in Rust. We
+will also be able to extract this model of core in every of our
+backends, enabling a uniform and pain-free <code>core</code> multi-backend
+library.</p><h1 id=merged-pull-requests>Merged Pull Requests<a hidden class=anchor aria-hidden=true href=#merged-pull-requests>#</a></h1><ul><li>#934: <a href=https://github.com/hacspec/hax/pull/934>chore: assign an issue id for every error in the engine</a></li><li>#932: <a href=https://github.com/hacspec/hax/pull/932>chore: assign an issue for every error in <code>import_thir</code></a></li><li>#919: <a href=https://github.com/hacspec/hax/pull/919>fix #422</a></li><li>#918: <a href=https://github.com/hacspec/hax/pull/918>chore: remove stale <code>Hax.Lib.fst</code></a></li><li>#917: <a href=https://github.com/hacspec/hax/pull/917>doc: disambiguate_local_idents</a></li><li>#916: <a href=https://github.com/hacspec/hax/pull/916>update Cargo.lock</a></li><li>#909: <a href=https://github.com/hacspec/hax/pull/909>Revert &ldquo;fix(engine/fstar): fix super typeclasses attributes&rdquo;</a></li><li>#908: <a href=https://github.com/hacspec/hax/pull/908>fix(engine/deps): stop re-computing over and over the set of assoc items</a></li><li>#907: <a href=https://github.com/hacspec/hax/pull/907>Add RewriteControlFlow phase.</a></li><li>#906: <a href=https://github.com/hacspec/hax/pull/906>Cleanup trait resolution</a></li><li>#902: <a href=https://github.com/hacspec/hax/pull/902>fix(engine/fstar): fix super typeclasses attributes</a></li><li>#901: <a href=https://github.com/hacspec/hax/pull/901>Determine emuerate value by index</a></li><li>#898: <a href=https://github.com/hacspec/hax/pull/898>Fix some binder-related crashes</a></li><li>#895: <a href=https://github.com/hacspec/hax/pull/895>Don&rsquo;t eval constants eagerly</a></li><li>#894: <a href=https://github.com/hacspec/hax/pull/894>Detangle trait solving from <code>SInto</code></a></li><li>#892: <a href=https://github.com/hacspec/hax/pull/892>Support other variants of MIR</a></li><li>#891: <a href=https://github.com/hacspec/hax/pull/891>fix: fstar: default trait</a></li><li>#887: <a href=https://github.com/hacspec/hax/pull/887>Initial cleanup of binders-related code</a></li><li>#885: <a href=https://github.com/hacspec/hax/pull/885>docs(book): depend on <code>hax-lib</code> only when using hax</a></li><li>#884: <a href=https://github.com/hacspec/hax/pull/884>Fix incorrect line numbers in error messages</a></li><li>#883: <a href=https://github.com/hacspec/hax/pull/883>Fix step boundaries in fold_range_step_by</a></li><li>#882: <a href=https://github.com/hacspec/hax/pull/882>fix(fstar-core): add support for <code>Option::map</code></a></li><li>#880: <a href=https://github.com/hacspec/hax/pull/880>Support float literals</a></li><li>#877: <a href=https://github.com/hacspec/hax/pull/877>Avoid recursing twice on the arguments.</a></li><li>#876: <a href=https://github.com/hacspec/hax/pull/876>Translate additional unsafe MIR operations</a></li><li>#873: <a href=https://github.com/hacspec/hax/pull/873>Small PR to fix circularity in Core.Fmt.fsti</a></li><li>#872: <a href=https://github.com/hacspec/hax/pull/872>Pre post impl blocks</a></li><li>#870: <a href=https://github.com/hacspec/hax/pull/870>count-ones post-condition</a></li><li>#868: <a href=https://github.com/hacspec/hax/pull/868>engine: kill a few <code>exn</code> to get useful errors</a></li><li>#867: <a href=https://github.com/hacspec/hax/pull/867>Backend: Import unsafe code as a gated feature</a></li><li>#860: <a href=https://github.com/hacspec/hax/pull/860>fix(engine): make dep. analysis sensible to UID assoc. items</a></li><li>#827: <a href=https://github.com/hacspec/hax/pull/827>Add infos impl</a></li><li>#819: <a href=https://github.com/hacspec/hax/pull/819>Add Rust Core Fstar Definitions.</a></li></ul><h4 id=contributors>Contributors<a hidden class=anchor aria-hidden=true href=#contributors>#</a></h4><ul><li><a href=https://github.com/Nadrieril>Nadrieril</a></li><li><a href=https://github.com/R1kM>R1kM</a></li><li><a href=https://github.com/ROMemories>ROMemories</a></li><li><a href=https://github.com/W95Psp>W95Psp</a></li><li><a href=https://github.com/franziskuskiefer>franziskuskiefer</a></li><li><a href=https://github.com/gaetan-sbt>gaetan-sbt</a></li><li><a href=https://github.com/karthikbhargavan>karthikbhargavan</a></li><li><a href=https://github.com/mamonet>mamonet</a></li><li><a href=https://github.com/maximebuyse>maximebuyse</a></li><li><a href=https://github.com/paulmure>paulmure</a></li></ul></div><footer class=post-footer><ul class=post-tags><li><a href=https://hacspec.github.io/blog/tags/this-month-in-hax/>this-month-in-hax</a></li></ul><nav class=paginav><a class=next href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-07/><span class=title>Next »</span><br><span>This month in hax: July 2024</span></a></nav></footer></article></main><footer class=footer><span>&copy; 2024 <a href=https://hacspec.github.io/blog/>hax</a></span>
+<span>Powered by
+<a href=https://gohugo.io/ rel="noopener noreferrer" target=_blank>Hugo</a> &
+        <a href=https://github.com/adityatelange/hugo-PaperMod/ rel=noopener target=_blank>PaperMod</a></span></footer><a href=#top aria-label="go to top" title="Go to Top (Alt + G)" class=top-link id=top-link accesskey=g><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 12 6" fill="currentcolor"><path d="M12 6H0l6-6z"/></svg></a><script>let menu=document.getElementById("menu");menu&&(menu.scrollLeft=localStorage.getItem("menu-scroll-position"),menu.onscroll=function(){localStorage.setItem("menu-scroll-position",menu.scrollLeft)}),document.querySelectorAll('a[href^="#"]').forEach(e=>{e.addEventListener("click",function(e){e.preventDefault();var t=this.getAttribute("href").substr(1);window.matchMedia("(prefers-reduced-motion: reduce)").matches?document.querySelector(`[id='${decodeURIComponent(t)}']`).scrollIntoView():document.querySelector(`[id='${decodeURIComponent(t)}']`).scrollIntoView({behavior:"smooth"}),t==="top"?history.replaceState(null,null," "):history.pushState(null,null,`#${t}`)})})</script><script>var mybutton=document.getElementById("top-link");window.onscroll=function(){document.body.scrollTop>800||document.documentElement.scrollTop>800?(mybutton.style.visibility="visible",mybutton.style.opacity="1"):(mybutton.style.visibility="hidden",mybutton.style.opacity="0")}</script><script>document.getElementById("theme-toggle").addEventListener("click",()=>{document.body.className.includes("dark")?(document.body.classList.remove("dark"),localStorage.setItem("pref-theme","light")):(document.body.classList.add("dark"),localStorage.setItem("pref-theme","dark"))})</script><script>document.querySelectorAll("pre > code").forEach(e=>{const n=e.parentNode.parentNode,t=document.createElement("button");t.classList.add("copy-code"),t.innerHTML="copy";function s(){t.innerHTML="copied!",setTimeout(()=>{t.innerHTML="copy"},2e3)}t.addEventListener("click",t=>{if("clipboard"in navigator){navigator.clipboard.writeText(e.textContent),s();return}const n=document.createRange();n.selectNodeContents(e);const o=window.getSelection();o.removeAllRanges(),o.addRange(n);try{document.execCommand("copy"),s()}catch{}o.removeRange(n)}),n.classList.contains("highlight")?n.appendChild(t):n.parentNode.firstChild==n||(e.parentNode.parentNode.parentNode.parentNode.parentNode.nodeName=="TABLE"?e.parentNode.parentNode.parentNode.parentNode.parentNode.appendChild(t):e.parentNode.appendChild(t))})</script></body></html>
\ No newline at end of file
diff --git a/sitemap.xml b/sitemap.xml
index 0853b84..55eadfc 100644
--- a/sitemap.xml
+++ b/sitemap.xml
@@ -3,18 +3,21 @@
   xmlns:xhtml="http://www.w3.org/1999/xhtml">
   <url>
     <loc>https://hacspec.github.io/blog/</loc>
-    <lastmod>2024-08-12T00:00:00+00:00</lastmod>
+    <lastmod>2024-10-01T00:00:00+00:00</lastmod>
   </url><url>
     <loc>https://hacspec.github.io/blog/posts/</loc>
-    <lastmod>2024-08-12T00:00:00+00:00</lastmod>
+    <lastmod>2024-10-01T00:00:00+00:00</lastmod>
   </url><url>
     <loc>https://hacspec.github.io/blog/tags/</loc>
-    <lastmod>2024-08-12T00:00:00+00:00</lastmod>
+    <lastmod>2024-10-01T00:00:00+00:00</lastmod>
   </url><url>
-    <loc>https://hacspec.github.io/blog/posts/this-month-in-hax/2024-07/</loc>
-    <lastmod>2024-08-12T00:00:00+00:00</lastmod>
+    <loc>https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/</loc>
+    <lastmod>2024-10-01T00:00:00+00:00</lastmod>
   </url><url>
     <loc>https://hacspec.github.io/blog/tags/this-month-in-hax/</loc>
+    <lastmod>2024-10-01T00:00:00+00:00</lastmod>
+  </url><url>
+    <loc>https://hacspec.github.io/blog/posts/this-month-in-hax/2024-07/</loc>
     <lastmod>2024-08-12T00:00:00+00:00</lastmod>
   </url><url>
     <loc>https://hacspec.github.io/blog/posts/this-month-in-hax/2024-06/</loc>
diff --git a/tags/index.html b/tags/index.html
index b751e31..ffdb4f6 100644
--- a/tags/index.html
+++ b/tags/index.html
@@ -1,5 +1,5 @@
 <!doctype html><html lang=en dir=auto><head><meta charset=utf-8><meta http-equiv=X-UA-Compatible content="IE=edge"><meta name=viewport content="width=device-width,initial-scale=1,shrink-to-fit=no"><meta name=robots content="index, follow"><title>Tags | hax</title>
-<meta name=keywords content><meta name=description content="hax & hacspec blog - https://github.com/hacspec/blog"><meta name=author content="hacspec authors"><link rel=canonical href=https://hacspec.github.io/blog/tags/><link crossorigin=anonymous href=/blog/assets/css/stylesheet.1b82bbed8b13f853704558d527b681efaea938ce91e6ae8903e8b19e73b1b0f8.css integrity="sha256-G4K77YsT+FNwRVjVJ7aB766pOM6R5q6JA+ixnnOxsPg=" rel="preload stylesheet" as=style><link rel=icon href=https://hacspec.github.io/blog/favicon.ico><link rel=icon type=image/png sizes=16x16 href=https://hacspec.github.io/blog/favicon-16x16.png><link rel=icon type=image/png sizes=32x32 href=https://hacspec.github.io/blog/favicon-32x32.png><link rel=apple-touch-icon href=https://hacspec.github.io/blog/apple-touch-icon.png><link rel=mask-icon href=https://hacspec.github.io/blog/safari-pinned-tab.svg><meta name=theme-color content="#2e2e33"><meta name=msapplication-TileColor content="#2e2e33"><link rel=alternate type=application/rss+xml href=https://hacspec.github.io/blog/tags/index.xml><noscript><style>#theme-toggle,.top-link{display:none}</style><style>@media(prefers-color-scheme:dark){:root{--theme:rgb(29, 30, 32);--entry:rgb(46, 46, 51);--primary:rgb(218, 218, 219);--secondary:rgb(155, 156, 157);--tertiary:rgb(65, 66, 68);--content:rgb(196, 196, 197);--hljs-bg:rgb(46, 46, 51);--code-bg:rgb(55, 56, 62);--border:rgb(51, 51, 51)}.list{background:var(--theme)}.list:not(.dark)::-webkit-scrollbar-track{background:0 0}.list:not(.dark)::-webkit-scrollbar-thumb{border-color:var(--theme)}}</style></noscript><meta property="og:title" content="Tags"><meta property="og:description" content="hax & hacspec blog - https://github.com/hacspec/blog"><meta property="og:type" content="website"><meta property="og:url" content="https://hacspec.github.io/blog/tags/"><meta property="og:image" content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:card content="summary_large_image"><meta name=twitter:image content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:title content="Tags"><meta name=twitter:description content="hax & hacspec blog - https://github.com/hacspec/blog"></head><body class=list id=top><script>localStorage.getItem("pref-theme")==="dark"?document.body.classList.add("dark"):localStorage.getItem("pref-theme")==="light"?document.body.classList.remove("dark"):window.matchMedia("(prefers-color-scheme: dark)").matches&&document.body.classList.add("dark")</script><header class=header><nav class=nav><div class=logo><a href=https://hacspec.github.io/blog/ accesskey=h title="hax (Alt + H)">hax</a><div class=logo-switches><button id=theme-toggle accesskey=t title="(Alt + T)"><svg id="moon" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M21 12.79A9 9 0 1111.21 3 7 7 0 0021 12.79z"/></svg><svg id="sun" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><circle cx="12" cy="12" r="5"/><line x1="12" y1="1" x2="12" y2="3"/><line x1="12" y1="21" x2="12" y2="23"/><line x1="4.22" y1="4.22" x2="5.64" y2="5.64"/><line x1="18.36" y1="18.36" x2="19.78" y2="19.78"/><line x1="1" y1="12" x2="3" y2="12"/><line x1="21" y1="12" x2="23" y2="12"/><line x1="4.22" y1="19.78" x2="5.64" y2="18.36"/><line x1="18.36" y1="5.64" x2="19.78" y2="4.22"/></svg></button></div></div><ul id=menu><li><a href=https://hacspec.github.io/blog/archives title=Archive><span>Archive</span></a></li><li><a href=https://hacspec.github.io/blog/search/ title="Search (Alt + /)" accesskey=/><span>Search</span></a></li><li><a href=https://hacspec.github.io/blog/tags/ title=Tags><span class=active>Tags</span></a></li></ul></nav></header><main class=main><header class=page-header><h1>Tags</h1></header><ul class=terms-tags><li><a href=https://hacspec.github.io/blog/tags/announcement/>announcement <sup><strong><sup>2</sup></strong></sup></a></li><li><a href=https://hacspec.github.io/blog/tags/release/>release <sup><strong><sup>1</sup></strong></sup></a></li><li><a href=https://hacspec.github.io/blog/tags/this-month-in-hax/>this-month-in-hax <sup><strong><sup>2</sup></strong></sup></a></li><li><a href=https://hacspec.github.io/blog/tags/tutorial/>tutorial <sup><strong><sup>1</sup></strong></sup></a></li></ul></main><footer class=footer><span>&copy; 2024 <a href=https://hacspec.github.io/blog/>hax</a></span>
+<meta name=keywords content><meta name=description content="hax & hacspec blog - https://github.com/hacspec/blog"><meta name=author content="hacspec authors"><link rel=canonical href=https://hacspec.github.io/blog/tags/><link crossorigin=anonymous href=/blog/assets/css/stylesheet.1b82bbed8b13f853704558d527b681efaea938ce91e6ae8903e8b19e73b1b0f8.css integrity="sha256-G4K77YsT+FNwRVjVJ7aB766pOM6R5q6JA+ixnnOxsPg=" rel="preload stylesheet" as=style><link rel=icon href=https://hacspec.github.io/blog/favicon.ico><link rel=icon type=image/png sizes=16x16 href=https://hacspec.github.io/blog/favicon-16x16.png><link rel=icon type=image/png sizes=32x32 href=https://hacspec.github.io/blog/favicon-32x32.png><link rel=apple-touch-icon href=https://hacspec.github.io/blog/apple-touch-icon.png><link rel=mask-icon href=https://hacspec.github.io/blog/safari-pinned-tab.svg><meta name=theme-color content="#2e2e33"><meta name=msapplication-TileColor content="#2e2e33"><link rel=alternate type=application/rss+xml href=https://hacspec.github.io/blog/tags/index.xml><noscript><style>#theme-toggle,.top-link{display:none}</style><style>@media(prefers-color-scheme:dark){:root{--theme:rgb(29, 30, 32);--entry:rgb(46, 46, 51);--primary:rgb(218, 218, 219);--secondary:rgb(155, 156, 157);--tertiary:rgb(65, 66, 68);--content:rgb(196, 196, 197);--hljs-bg:rgb(46, 46, 51);--code-bg:rgb(55, 56, 62);--border:rgb(51, 51, 51)}.list{background:var(--theme)}.list:not(.dark)::-webkit-scrollbar-track{background:0 0}.list:not(.dark)::-webkit-scrollbar-thumb{border-color:var(--theme)}}</style></noscript><meta property="og:title" content="Tags"><meta property="og:description" content="hax & hacspec blog - https://github.com/hacspec/blog"><meta property="og:type" content="website"><meta property="og:url" content="https://hacspec.github.io/blog/tags/"><meta property="og:image" content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:card content="summary_large_image"><meta name=twitter:image content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:title content="Tags"><meta name=twitter:description content="hax & hacspec blog - https://github.com/hacspec/blog"></head><body class=list id=top><script>localStorage.getItem("pref-theme")==="dark"?document.body.classList.add("dark"):localStorage.getItem("pref-theme")==="light"?document.body.classList.remove("dark"):window.matchMedia("(prefers-color-scheme: dark)").matches&&document.body.classList.add("dark")</script><header class=header><nav class=nav><div class=logo><a href=https://hacspec.github.io/blog/ accesskey=h title="hax (Alt + H)">hax</a><div class=logo-switches><button id=theme-toggle accesskey=t title="(Alt + T)"><svg id="moon" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M21 12.79A9 9 0 1111.21 3 7 7 0 0021 12.79z"/></svg><svg id="sun" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><circle cx="12" cy="12" r="5"/><line x1="12" y1="1" x2="12" y2="3"/><line x1="12" y1="21" x2="12" y2="23"/><line x1="4.22" y1="4.22" x2="5.64" y2="5.64"/><line x1="18.36" y1="18.36" x2="19.78" y2="19.78"/><line x1="1" y1="12" x2="3" y2="12"/><line x1="21" y1="12" x2="23" y2="12"/><line x1="4.22" y1="19.78" x2="5.64" y2="18.36"/><line x1="18.36" y1="5.64" x2="19.78" y2="4.22"/></svg></button></div></div><ul id=menu><li><a href=https://hacspec.github.io/blog/archives title=Archive><span>Archive</span></a></li><li><a href=https://hacspec.github.io/blog/search/ title="Search (Alt + /)" accesskey=/><span>Search</span></a></li><li><a href=https://hacspec.github.io/blog/tags/ title=Tags><span class=active>Tags</span></a></li></ul></nav></header><main class=main><header class=page-header><h1>Tags</h1></header><ul class=terms-tags><li><a href=https://hacspec.github.io/blog/tags/announcement/>announcement <sup><strong><sup>2</sup></strong></sup></a></li><li><a href=https://hacspec.github.io/blog/tags/release/>release <sup><strong><sup>1</sup></strong></sup></a></li><li><a href=https://hacspec.github.io/blog/tags/this-month-in-hax/>this-month-in-hax <sup><strong><sup>3</sup></strong></sup></a></li><li><a href=https://hacspec.github.io/blog/tags/tutorial/>tutorial <sup><strong><sup>1</sup></strong></sup></a></li></ul></main><footer class=footer><span>&copy; 2024 <a href=https://hacspec.github.io/blog/>hax</a></span>
 <span>Powered by
 <a href=https://gohugo.io/ rel="noopener noreferrer" target=_blank>Hugo</a> &
         <a href=https://github.com/adityatelange/hugo-PaperMod/ rel=noopener target=_blank>PaperMod</a></span></footer><a href=#top aria-label="go to top" title="Go to Top (Alt + G)" class=top-link id=top-link accesskey=g><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 12 6" fill="currentcolor"><path d="M12 6H0l6-6z"/></svg></a><script>let menu=document.getElementById("menu");menu&&(menu.scrollLeft=localStorage.getItem("menu-scroll-position"),menu.onscroll=function(){localStorage.setItem("menu-scroll-position",menu.scrollLeft)}),document.querySelectorAll('a[href^="#"]').forEach(e=>{e.addEventListener("click",function(e){e.preventDefault();var t=this.getAttribute("href").substr(1);window.matchMedia("(prefers-reduced-motion: reduce)").matches?document.querySelector(`[id='${decodeURIComponent(t)}']`).scrollIntoView():document.querySelector(`[id='${decodeURIComponent(t)}']`).scrollIntoView({behavior:"smooth"}),t==="top"?history.replaceState(null,null," "):history.pushState(null,null,`#${t}`)})})</script><script>var mybutton=document.getElementById("top-link");window.onscroll=function(){document.body.scrollTop>800||document.documentElement.scrollTop>800?(mybutton.style.visibility="visible",mybutton.style.opacity="1"):(mybutton.style.visibility="hidden",mybutton.style.opacity="0")}</script><script>document.getElementById("theme-toggle").addEventListener("click",()=>{document.body.className.includes("dark")?(document.body.classList.remove("dark"),localStorage.setItem("pref-theme","light")):(document.body.classList.add("dark"),localStorage.setItem("pref-theme","dark"))})</script></body></html>
\ No newline at end of file
diff --git a/tags/index.xml b/tags/index.xml
index d024e15..03a5cfa 100644
--- a/tags/index.xml
+++ b/tags/index.xml
@@ -11,11 +11,11 @@
     </image>
     <generator>Hugo -- gohugo.io</generator>
     <language>en</language>
-    <lastBuildDate>Mon, 12 Aug 2024 00:00:00 +0000</lastBuildDate><atom:link href="https://hacspec.github.io/blog/tags/index.xml" rel="self" type="application/rss+xml" />
+    <lastBuildDate>Tue, 01 Oct 2024 00:00:00 +0000</lastBuildDate><atom:link href="https://hacspec.github.io/blog/tags/index.xml" rel="self" type="application/rss+xml" />
     <item>
       <title>this-month-in-hax</title>
       <link>https://hacspec.github.io/blog/tags/this-month-in-hax/</link>
-      <pubDate>Mon, 12 Aug 2024 00:00:00 +0000</pubDate>
+      <pubDate>Tue, 01 Oct 2024 00:00:00 +0000</pubDate>
       
       <guid>https://hacspec.github.io/blog/tags/this-month-in-hax/</guid>
       <description></description>
diff --git a/tags/this-month-in-hax/index.html b/tags/this-month-in-hax/index.html
index 60d4d12..57355d1 100644
--- a/tags/this-month-in-hax/index.html
+++ b/tags/this-month-in-hax/index.html
@@ -1,6 +1,8 @@
 <!doctype html><html lang=en dir=auto><head><meta charset=utf-8><meta http-equiv=X-UA-Compatible content="IE=edge"><meta name=viewport content="width=device-width,initial-scale=1,shrink-to-fit=no"><meta name=robots content="index, follow"><title>this-month-in-hax | hax</title>
 <meta name=keywords content><meta name=description content="hax & hacspec blog - https://github.com/hacspec/blog"><meta name=author content="hacspec authors"><link rel=canonical href=https://hacspec.github.io/blog/tags/this-month-in-hax/><link crossorigin=anonymous href=/blog/assets/css/stylesheet.1b82bbed8b13f853704558d527b681efaea938ce91e6ae8903e8b19e73b1b0f8.css integrity="sha256-G4K77YsT+FNwRVjVJ7aB766pOM6R5q6JA+ixnnOxsPg=" rel="preload stylesheet" as=style><link rel=icon href=https://hacspec.github.io/blog/favicon.ico><link rel=icon type=image/png sizes=16x16 href=https://hacspec.github.io/blog/favicon-16x16.png><link rel=icon type=image/png sizes=32x32 href=https://hacspec.github.io/blog/favicon-32x32.png><link rel=apple-touch-icon href=https://hacspec.github.io/blog/apple-touch-icon.png><link rel=mask-icon href=https://hacspec.github.io/blog/safari-pinned-tab.svg><meta name=theme-color content="#2e2e33"><meta name=msapplication-TileColor content="#2e2e33"><link rel=alternate type=application/rss+xml href=https://hacspec.github.io/blog/tags/this-month-in-hax/index.xml><noscript><style>#theme-toggle,.top-link{display:none}</style><style>@media(prefers-color-scheme:dark){:root{--theme:rgb(29, 30, 32);--entry:rgb(46, 46, 51);--primary:rgb(218, 218, 219);--secondary:rgb(155, 156, 157);--tertiary:rgb(65, 66, 68);--content:rgb(196, 196, 197);--hljs-bg:rgb(46, 46, 51);--code-bg:rgb(55, 56, 62);--border:rgb(51, 51, 51)}.list{background:var(--theme)}.list:not(.dark)::-webkit-scrollbar-track{background:0 0}.list:not(.dark)::-webkit-scrollbar-thumb{border-color:var(--theme)}}</style></noscript><meta property="og:title" content="this-month-in-hax"><meta property="og:description" content="hax & hacspec blog - https://github.com/hacspec/blog"><meta property="og:type" content="website"><meta property="og:url" content="https://hacspec.github.io/blog/tags/this-month-in-hax/"><meta property="og:image" content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:card content="summary_large_image"><meta name=twitter:image content="https://hacspec.github.io/blog/papermod-cover.png"><meta name=twitter:title content="this-month-in-hax"><meta name=twitter:description content="hax & hacspec blog - https://github.com/hacspec/blog"></head><body class=list id=top><script>localStorage.getItem("pref-theme")==="dark"?document.body.classList.add("dark"):localStorage.getItem("pref-theme")==="light"?document.body.classList.remove("dark"):window.matchMedia("(prefers-color-scheme: dark)").matches&&document.body.classList.add("dark")</script><header class=header><nav class=nav><div class=logo><a href=https://hacspec.github.io/blog/ accesskey=h title="hax (Alt + H)">hax</a><div class=logo-switches><button id=theme-toggle accesskey=t title="(Alt + T)"><svg id="moon" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><path d="M21 12.79A9 9 0 1111.21 3 7 7 0 0021 12.79z"/></svg><svg id="sun" xmlns="http://www.w3.org/2000/svg" width="24" height="18" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round"><circle cx="12" cy="12" r="5"/><line x1="12" y1="1" x2="12" y2="3"/><line x1="12" y1="21" x2="12" y2="23"/><line x1="4.22" y1="4.22" x2="5.64" y2="5.64"/><line x1="18.36" y1="18.36" x2="19.78" y2="19.78"/><line x1="1" y1="12" x2="3" y2="12"/><line x1="21" y1="12" x2="23" y2="12"/><line x1="4.22" y1="19.78" x2="5.64" y2="18.36"/><line x1="18.36" y1="5.64" x2="19.78" y2="4.22"/></svg></button></div></div><ul id=menu><li><a href=https://hacspec.github.io/blog/archives title=Archive><span>Archive</span></a></li><li><a href=https://hacspec.github.io/blog/search/ title="Search (Alt + /)" accesskey=/><span>Search</span></a></li><li><a href=https://hacspec.github.io/blog/tags/ title=Tags><span>Tags</span></a></li></ul></nav></header><main class=main><header class=page-header><div class=breadcrumbs><a href=https://hacspec.github.io/blog/>Home</a>&nbsp;»&nbsp;<a href=https://hacspec.github.io/blog/tags/>Tags</a></div><h1>this-month-in-hax
-<a href=/blog/tags/this-month-in-hax/index.xml title=RSS aria-label=RSS><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" height="23"><path d="M4 11a9 9 0 019 9"/><path d="M4 4a16 16 0 0116 16"/><circle cx="5" cy="19" r="1"/></svg></a></h1></header><article class="post-entry tag-entry"><header class=entry-header><h2>This month in hax: July 2024</h2></header><div class=entry-content><p>In July, we merged 32 PRs! 🎉
+<a href=/blog/tags/this-month-in-hax/index.xml title=RSS aria-label=RSS><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" fill="none" stroke="currentcolor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round" height="23"><path d="M4 11a9 9 0 019 9"/><path d="M4 4a16 16 0 0116 16"/><circle cx="5" cy="19" r="1"/></svg></a></h1></header><article class="post-entry tag-entry"><header class=entry-header><h2>This month in hax: September 2024</h2></header><div class=entry-content><p>In July, we merged 33 PRs! 🎉
+On the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. 'a in for&lt;'a> &'a T: PartialEq&lt;i32>) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code.
+In the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue....</p></div><footer class=entry-footer><span title='2024-10-01 00:00:00 +0000 UTC'>October 1, 2024</span>&nbsp;·&nbsp;2 min&nbsp;·&nbsp;Lucas Franceschino</footer><a class=entry-link aria-label="post link to This month in hax: September 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/></a></article><article class="post-entry tag-entry"><header class=entry-header><h2>This month in hax: July 2024</h2></header><div class=entry-content><p>In July, we merged 32 PRs! 🎉
 On the side of the frontend and CLI, we had a lot of fixes and improvements! The hax command line and rustc driver were refactored, allowing for better scaling and caching. We also improved the general ergonomics: diagnostics can now be output in JSON, we have improved error messages… And we pushed various bug fixes.
 In the engine, we now resugar asserts properly and support dyn....</p></div><footer class=entry-footer><span title='2024-08-12 00:00:00 +0000 UTC'>August 12, 2024</span>&nbsp;·&nbsp;2 min&nbsp;·&nbsp;Lucas Franceschino</footer><a class=entry-link aria-label="post link to This month in hax: July 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-07/></a></article><article class="post-entry tag-entry"><header class=entry-header><h2>This month in hax: June 2024</h2></header><div class=entry-content><p>This first blog post inaugurates our series named “This Month in hax”: a series of short highlights of what happened in the development of hax and it’s ecosystem in the month.
 In June, 23 PRs have been merged 🎉! The detail is available below.
diff --git a/tags/this-month-in-hax/index.xml b/tags/this-month-in-hax/index.xml
index b167f3c..cd377d5 100644
--- a/tags/this-month-in-hax/index.xml
+++ b/tags/this-month-in-hax/index.xml
@@ -11,7 +11,18 @@
     </image>
     <generator>Hugo -- gohugo.io</generator>
     <language>en</language>
-    <lastBuildDate>Mon, 12 Aug 2024 00:00:00 +0000</lastBuildDate><atom:link href="https://hacspec.github.io/blog/tags/this-month-in-hax/index.xml" rel="self" type="application/rss+xml" />
+    <lastBuildDate>Tue, 01 Oct 2024 00:00:00 +0000</lastBuildDate><atom:link href="https://hacspec.github.io/blog/tags/this-month-in-hax/index.xml" rel="self" type="application/rss+xml" />
+    <item>
+      <title>This month in hax: September 2024</title>
+      <link>https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/</link>
+      <pubDate>Tue, 01 Oct 2024 00:00:00 +0000</pubDate>
+      
+      <guid>https://hacspec.github.io/blog/posts/this-month-in-hax/2024-09/</guid>
+      <description>In July, we merged 33 PRs! 🎉
+On the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. &#39;a in for&amp;lt;&#39;a&amp;gt; &amp;amp;&#39;a T: PartialEq&amp;lt;i32&amp;gt;) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code.
+In the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue.</description>
+    </item>
+    
     <item>
       <title>This month in hax: July 2024</title>
       <link>https://hacspec.github.io/blog/posts/this-month-in-hax/2024-07/</link>
