From d02476d9257e4d899d26bacc73b7a14312aba9e9 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Mon, 25 Aug 2025 23:01:46 -0700 Subject: [PATCH] link to issue and project --- nlnet-2024-12-324/progress.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/nlnet-2024-12-324/progress.md b/nlnet-2024-12-324/progress.md index e29d4ec..6fb94fb 100644 --- a/nlnet-2024-12-324/progress.md +++ b/nlnet-2024-12-324/progress.md @@ -4,6 +4,8 @@ See Notices.txt for copyright information --> # NLnet 2024-12-324 Grant Progress +[Forgejo Project for this grant.](https://git.libre-chip.org/libre-chip/grant-tracking/projects/1) + # € 50000 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs Modern computers suffer from a constant stream of new speculative-execution security flaws (Spectre-style bugs). To address this major category of flaws, we are working towards building a high-performance computer processor (CPU) with speculative execution and working on a mathematical proof that it doesn't suffer from any speculative-execution data leaks, thereby demonstrating that this major category of flaws can be eliminated without crippling the computer's performance. @@ -14,7 +16,7 @@ https://en.wikipedia.org/wiki/Transient_execution_CPU_vulnerability#Timeline This is for adding the code for translating Fayalite HDL to Rocq, as well as determining how exactly we'll describe HDL in Rocq. I expect the translation code to be of comparable size to the compiler portion of the simulator (the simulator is broken into three main parts, a compiler to an IR optimized for interpretation, the interpreter itself, and the code for reading/writing simulator I/O and handling time simulation), so somewhere around 5000 LoC. -- € 2000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Figure out how exactly we should represent HDL in Rocq, writing down a manually-translated version of common HDL components (e.g. how to translate a register, a memory, an add/sub/mul/div, etc.). +- € 2000 [Issue #2](https://git.libre-chip.org/libre-chip/grant-tracking/issues/2) Figure out how exactly we should represent HDL in Rocq, writing down a manually-translated version of common HDL components (e.g. how to translate a register, a memory, an add/sub/mul/div, etc.). - € 4000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Write the code to do the translation in Fayalite. ## € 4000 Adding supporting code for generating FPGA bitstreams from Fayalite