add link to WIP high-level CPU design

src/grants/nlnet-first.md

@@ -55,7 +55,9 @@ To address this general category of CPU flaws, I (Jacob Lifshay) invented a way
 2. Take the concrete cycle-accurate CPU design, and construct a theoretical equivalent that has the additional feature of looking into the future to determine which instructions will be canceled and preemptively forces their results to be zeros (or any other value that doesn't depend on transient instructions' data; since we're doing math here, we don't have to limit ourselves to physically possible designs that respect time flow). The reasoning is that if all transient instructions' results are always zeros, they can't possibly be leaking any useful data, therefore the theoretical equivalent CPU design doesn't have any speculative-execution data leaks.
 3. Formally prove that all digital signals from/to the concrete CPU core always exactly match the timing and data in all respects of the theoretical equivalent CPU design. This proves that the concrete CPU core can't have any speculative-execution data leaks.
 
-It is expected that automated formal proof software (stuff like SMT solvers such as Z3) will probably be too slow to be usable for the formal correctness proof, therefore the plan is to use Fayalite to generate a translation of the CPU design to Coq or some other similar language for writing formal proofs. [Fayalite](https://git.libre-chip.org/libre-chip/fayalite) is a HDL library written in Rust that we have been developing since around April 2024 that targets the [FIRRTL](https://github.com/chipsalliance/firrtl-spec) intermediate language (used by the [Chisel](https://www.chisel-lang.org/) ecosystem for generating Verilog; firtool, the FIRRTL to Verilog translator, is part of [LLVM Circt](https://circt.llvm.org/), so is well maintained):
+It is expected that automated formal proof software (stuff like SMT solvers such as Z3) will probably be too slow to be usable for the formal correctness proof, therefore the plan is to use Fayalite to generate a translation of the CPU design to Coq or some other similar language for writing formal proofs. [Fayalite](https://git.libre-chip.org/libre-chip/fayalite) is a HDL library written in Rust that we have been developing since around April 2024 that targets the [FIRRTL](https://github.com/chipsalliance/firrtl-spec) intermediate language (used by the [Chisel](https://www.chisel-lang.org/) ecosystem for generating Verilog; firtool, the FIRRTL to Verilog translator, is part of [LLVM Circt](https://circt.llvm.org/), so is well maintained).
+
+A WIP high-level design of our CPU: <https://libre-chip.org/first_arch/index.html>
 
 ## Ecosystem