-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
df8d6ab
commit c382926
Showing
10 changed files
with
19 additions
and
19 deletions.
There are no files selected for viewing
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -2,7 +2,7 @@ | |
<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:[email protected]"]}</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:[email protected] 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: December 2024</h2></header><div class=entry-content><p>This is the last post of this series for 2024. | ||
During this somewhat brief December, as many take time off for the holidays, we merged 21 PRs. | ||
The focus this month was largely on bug fixes, improvements, and general cleanups, with most of the work concentrated on the engine. However, a few frontend updates made their way in as well. | ||
A notable contribution from @maximebuyse introduces more consistent support for marking Rust items as opaque, establishing a unified approach to opaqueness across nearly all types of Rust items....</p></div><footer class=entry-footer><span title='2024-12-06 00:00:00 +0000 UTC'>December 6, 2024</span> · 2 min · Lucas Franceschino</footer><a class=entry-link aria-label="post link to This month in hax: December 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-12/></a></article><article class=post-entry><header class=entry-header><h2>This month in hax: November 2024</h2></header><div class=entry-content><p>Despite some team members attending an offsite work week event, we merged 24 PRs this month. Here’s an overview of the work of the month. | ||
A notable contribution from @maximebuyse introduces more consistent support for marking Rust items as opaque, establishing a unified approach to opaqueness across nearly all types of Rust items....</p></div><footer class=entry-footer><span title='2025-01-06 00:00:00 +0000 UTC'>January 6, 2025</span> · 2 min · Lucas Franceschino</footer><a class=entry-link aria-label="post link to This month in hax: December 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-12/></a></article><article class=post-entry><header class=entry-header><h2>This month in hax: November 2024</h2></header><div class=entry-content><p>Despite some team members attending an offsite work week event, we merged 24 PRs this month. Here’s an overview of the work of the month. | ||
The frontend remained stable this month, with only a few pull requests focused on small improvements and bug fixes. Our CI now tests the extraction of Rust by Example. | ||
cmester0 is working on an annotated core library, which is extractable via hax to multiple backends. The Coq backend now uses this generated core library, and ships with an example....</p></div><footer class=entry-footer><span title='2024-12-03 00:00:00 +0000 UTC'>December 3, 2024</span> · 2 min · Lucas Franceschino</footer><a class=entry-link aria-label="post link to This month in hax: November 2024" href=https://hacspec.github.io/blog/posts/this-month-in-hax/2024-11/></a></article><article class=post-entry><header class=entry-header><h2>This month in hax: October 2024</h2></header><div class=entry-content><p>In October, we merged 70 PRs! 🎉 | ||
Thanks to a huge work from Nadrieril on trait resolution, the goal of handling all valid Rust code with hax frontend is now almost achieved. With these improvements and some bugfixes from W95Psp, we now produce JSON without errors for more than 99% of Rust’s top 800 crates! | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.