add estimated budget

src/grants/nlnet-first.md

@@ -26,7 +26,45 @@ Requested Amount €50000
 
 Nearly all of the cost is for labor, with some amount set aside for general project management (e.g. tracking funding, server maintenance, etc.), and for hardware costs such as buying bigger FPGAs so the CPU design will fit.
 
-TODO, come up with estimated budgets.
+We're aiming for a rate of somewhere around $69305.60/yr per person which is the minimum salary for small employers for 2025 in Washington State USA (where Jacob Lifshay lives). <https://www.lni.wa.gov/forms-publications/f700-207-000.pdf>
+
+Estimated Budget:
+
+### General Project Management
+
+&euro;2000
+
+For tracking funding, server maintenance, and similar.
+
+### Hardware Costs
+
+&euro;3000
+
+For buying bigger FPGAs, CI server hardware improvements, Oscilloscopes (if necessary), and similar.
+
+### Improvements to Fayalite
+
+&euro;10000
+
+For adding the code for translation to Coq, adding tooling for generating FPGA bitstreams, as well as other improvements to Fayalite as necessary.
+
+### Building enough of the CPU to execute multiple instructions
+
+&euro;10000
+
+This covers getting register renaming and ALU and/or branch instructions working, as well as other portions of the CPU design as necessary. This may or may not include actually fetching those instructions from memory, instead the instructions may be supplied by a testing harness.
+
+### Implementing Memory Subsystem
+
+&euro;15000
+
+This covers the rest needed for the CPU to be able to fetch instructions from memory and execute them as well as implementing Load/Store instructions.
+
+### Work towards the Formal Proof of No Spectre bugs
+
+&euro;10000
+
+This covers working on the Formal Proof of No Spectre bugs as well as improvements to other software/hardware needed for that.
 
 ## Compare with existing/historical efforts
 
@@ -46,7 +84,7 @@ Contract Shadow Logic works by assuming that memory is partitioned into secret a
 
 We expect to solve 2 technical challenges:
 
-* To create a working OoO Superscalar CPU with Speculative Execution, trying to design it such that it doesn't have any Spectre-style vulnerabilities (mostly by doing a better job of tracking any state whatsoever that has speculative modifications).
+* To create a working OoO Superscalar CPU with Speculative Execution, trying to design it such that it doesn't have any Spectre-style vulnerabilities (mostly by doing a better job of tracking any state whatsoever that has speculative modifications). The CPU probably will not yet support some of the features required for high performance (e.g. a complex cache hierarchy) and/or supporting running an operating system and/or floating-point. The plan is to add those features later if they are not completed as part of this grant.
 * To make substantial progress on creating a formal proof that the CPU doesn't have any Spectre-style vulnerabilities. This is complex enough and has enough potential problems we may run into that we may not finish by the end of this grant, and may need additional grants afterward to finish, hence why the goal is making substantial progress instead of having the proof 100% complete and working.
 
 To address this general category of CPU flaws, I (Jacob Lifshay) invented a way to formally prove that a CPU with speculative execution doesn't suffer from any speculative-execution data leaks: